arnekeller/Typicalc
1
0
Fork 0
mirror of https://gitlab.kit.edu/uskyk/typicalc.git synced 2024-11-08 10:20:41 +00:00
Code Issues Packages Projects Releases Wiki Activity

Fix Var and Const definitions and tooltips

Browse Source
This commit is contained in:
Arne Keller 2021-08-08 18:28:22 +02:00
parent a7a587a769
commit 69479a6368
3 changed files with 15 additions and 20 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
frontend/src/mathjax-proof-tree.ts
View File

@ -443,6 +443,7 @@ class MathjaxProofTree extends MathjaxAdapter {
.then(() => {
const svgP = p.getElementsByTagName("svg")[0];
const relevantElement = svgP.childNodes[1]! as SVGGraphicsElement;
const relevantElementBox = relevantElement.getBBox();
const relevantDefs = svgP.childNodes[0]!;
const ourDefs = svg.getElementsByTagName("defs")[0];
while (relevantDefs.childNodes.length > 0) {
@ -454,24 +455,19 @@ class MathjaxProofTree extends MathjaxAdapter {
for (const explainer of explainers) {
explainer.parentNode!.removeChild(explainer);
}
relevantElement.classList.add(hoverTextElID);
const x = String(-transform.e - svgRect.width + 30500);
const y = -transform.f - 4000;
const prevTransform = relevantElement.getAttribute("transform");
const newTranslate = "translate(" + x + ", " + y + ")";
const newTransform = prevTransform + " " + newTranslate;
relevantElement.setAttribute("transform", newTransform);
const g = insertionTarget.ownerDocument.createElementNS("http://www.w3.org/2000/svg", "g");
g.setAttribute("transform", "matrix(1 0 0 -1 0 0)");
g.transform.baseVal[0].matrix.f -= relevantElementBox.height / 2 + svgRect.height;
let ttBackground = document.createElementNS("http://www.w3.org/2000/svg", "rect");
ttBackground.classList.add(hoverTextElID);
g.classList.add(hoverTextElID);
const bbox = relevantElement.getBBox();
const newTranslate2 = "translate(" + x + ", " + (y - bbox.height / 2) + ")";
const newTransform2 = prevTransform + " " + newTranslate2;
ttBackground.setAttribute("transform", newTransform2);
ttBackground.setAttribute("width", String(bbox.width + 2000));
ttBackground.setAttribute("height", String(bbox.height + 1000));
ttBackground.setAttribute("transform", "translate(0 " + String(-bbox.height + 600) + ")");
ttBackground.setAttribute("fill", "yellow");
insertionTarget.appendChild(ttBackground);
insertionTarget.appendChild(relevantElement);
g.appendChild(ttBackground);
g.appendChild(relevantElement);
defEl.appendChild(g);
thisShadowRoot.removeChild(p);
});
this.shadowRoot!.appendChild(p);

5
src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java
View File

@ -75,14 +75,13 @@ public class StepAnnotator implements StepVisitor {
@Override
public void visit(ConstStepDefault constD) {
visitGeneric2(List.of(Pair.of("_c", constD.getConclusion().getType())), constD.getConstraint());
visitGeneric2(List.of(Pair.of("", constD.getConstraint().getSecondType())), constD.getConstraint());
}
@Override
public void visit(VarStepDefault varD) {
visitGeneric2(List.of(
Pair.of("", varD.getInstantiatedTypeAbs()),
Pair.of("'", varD.getConclusion().getType())),
Pair.of("", varD.getInstantiatedTypeAbs())),
varD.getConstraint());
}

8
src/main/resources/language/general.properties
View File

@ -16,7 +16,7 @@ root.exampleTerms=\
(λx.λy.y (x y)) (λz. λa. z g a),\
let f = λx. let g = λy. y in g x in f 3,\
let f = λx. let g = λy.5 5 in g x in f 3
root.λx.x=∅
root.λx.λy.yx=∅
root.(λx.xtrue)(yg)=∅;y: int->boolean->τ₁, g: boolean;y: int->boolean->τ₁, g: τ₁;y: int->boolean->τ₁, g: ∀τ₁.τ₁
@ -27,7 +27,7 @@ root.(λx.xx)(λx.xx)=∅
root.(λx.λy.y(xy))(λz.λa.zga)=∅;g: boolean;a: int, g: boolean->int;g: ∀τ₂.τ₁->τ₂
root.letfλx.letgλy.yingxinf3=∅;g: boolean->int->boolean
root.letfλx.letgλy.55ingxinf3=∅
root.termGrammar=\u2329Term\u232A ::= (\u2329Term\u232A) | \u2329App\u232A | \u2329Abs\u232A | \
\u2329Let\u232A | \u2329Var\u232A | \u2329Const\u232A <br> \
\u2329App\u232A ::= \u2329Term\u232A \u2329Term\u232A <br> \
@ -68,7 +68,7 @@ root.varLatex=\
\\AxiomC{$\\Gamma (\\texttt{x}) = \\tau$}\
\
\\LeftLabel{\\textrm V{\\small AR}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau'$}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
\\end{prooftree}
root.constLatex=\
@ -76,7 +76,7 @@ root.constLatex=\
\\AxiomC{$\\texttt{c} \\in Const$}\
\
\\LeftLabel{\\textrm C{\\small ONST}}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau_c$}\
\\UnaryInfC{$\\Gamma \\vdash \\texttt{c} : \\tau$}\
\\end{prooftree}
root.letLatex=\