From 69479a63688f9068e631ccc1b01112ea952d2b77 Mon Sep 17 00:00:00 2001 From: Arne Keller Date: Sun, 8 Aug 2021 18:28:22 +0200 Subject: [PATCH] Fix Var and Const definitions and tooltips --- frontend/src/mathjax-proof-tree.ts | 22 ++++++++----------- .../typicalc/model/step/StepAnnotator.java | 5 ++--- .../resources/language/general.properties | 8 +++---- 3 files changed, 15 insertions(+), 20 deletions(-) diff --git a/frontend/src/mathjax-proof-tree.ts b/frontend/src/mathjax-proof-tree.ts index fe79e35..c321de7 100644 --- a/frontend/src/mathjax-proof-tree.ts +++ b/frontend/src/mathjax-proof-tree.ts @@ -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); diff --git a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java index 4bc0e84..6ee6c7f 100644 --- a/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java +++ b/src/main/java/edu/kit/typicalc/model/step/StepAnnotator.java @@ -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()); } diff --git a/src/main/resources/language/general.properties b/src/main/resources/language/general.properties index 02ea1f3..21446da 100644 --- a/src/main/resources/language/general.properties +++ b/src/main/resources/language/general.properties @@ -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
\ \u2329App\u232A ::= \u2329Term\u232A \u2329Term\u232A
\ @@ -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=\