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

Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc

Browse Source
This commit is contained in:
ucrhh 2021-02-06 10:59:12 +01:00
commit bc30971b86
6 changed files with 22 additions and 44 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -26,9 +26,10 @@ class MathjaxProofTree extends MathjaxAdapter {
protected calculateSteps(): void {
if (this.shadowRoot !== null) {
const root = this.shadowRoot;
let semanticsMatch = (semantics: string) => semantics.indexOf("bspr_inference:") >= 0;
// first, enumerate all of the steps
let nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
let nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
let steps = [];
let a = null;
let stepIdx = 0;
@ -44,7 +45,7 @@ class MathjaxProofTree extends MathjaxAdapter {
}
}
// then fix some more mathjax layout issues
for (const step of this.shadowRoot.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
for (const step of root.querySelectorAll<HTMLElement>('g[typicalc="step"]')) {
const infRule = step.querySelector<HTMLElement>('g[semantics="bspr_inferenceRule:down"]');
if (infRule === null) {
continue;
@ -78,7 +79,7 @@ class MathjaxProofTree extends MathjaxAdapter {
stepAbove.transform.baseVal[0].matrix.e -= dx;
}
// then create the steps
nodeIterator = document.createNodeIterator(this.shadowRoot, NodeFilter.SHOW_ELEMENT);
nodeIterator = document.createNodeIterator(root, NodeFilter.SHOW_ELEMENT);
steps = [];
stepIdx = 0;
while (a = nodeIterator.nextNode() as HTMLElement) {
@ -122,7 +123,7 @@ class MathjaxProofTree extends MathjaxAdapter {
steps.push([a, above]);
}
}
const svg = this.shadowRoot.querySelector<SVGElement>("svg")!;
const svg = root.querySelector<SVGElement>("svg")!;
const nodeIterator2 = [...svg.querySelectorAll<SVGGraphicsElement>("g[data-mml-node='mtr']")];
// start layout fixes in the innermost part of the SVG
nodeIterator2.reverse();
@ -170,9 +171,9 @@ class MathjaxProofTree extends MathjaxAdapter {
i += 1;
}
}
const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
// TODO: this does not work when using a permalink
svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
// TODO: this does not scale the SVG correctly
//const bbox = (svg.childNodes[1] as SVGGraphicsElement).getBBox();
//svg.setAttribute("viewBox", bbox.x + " " + bbox.y + " " + bbox.width + " " + bbox.height);
if (counter >= 3) {
// should not be used on empty SVGs
// @ts-ignore

13
frontend/styles/view/main/input-bar.css
View File

@ -1,13 +1,5 @@
@media (max-width: 500px) {
#inputField {
width: 20em;
}
}
@media (min-width: 1000px) {
#inputField {
width: 30em;
}
#inputField {
flex-grow: 1;
}
#inputField {
@ -16,6 +8,7 @@
#inputBar {
align-items: center;
padding: 1em;
}
vaadin-drawer-toggle {

26
frontend/styles/view/main/upper-bar.css
View File

@ -19,31 +19,13 @@
}
#helpIcon {
margin-left: auto;
margin-left: 1em;
margin-right: 1em;
}
@media (max-width: 500px) {
#inputBar {
margin: auto;
}
#viewTitle {
margin-right: 5em;
}
}
@media (min-width: 1000px) {
#inputBar {
margin-left: 15em;
}
#viewTitle {
margin-right: auto;
}
#inputBar {
flex-grow: 1;
justify-content: end;
}

3
src/main/java/edu/kit/typicalc/model/TypeInferenceResult.java
View File

@ -63,9 +63,6 @@ public class TypeInferenceResult {
}
}
return typeVar;
// TODO: correct?
// throw new IllegalStateException("MGU has to contain substitution for original type variable: "
// + typeVar.toString());
}
/**

2
src/main/java/edu/kit/typicalc/view/main/ExampleDialog.java
View File

@ -23,7 +23,7 @@ public class ExampleDialog extends Dialog implements LocaleChangeObserver {
private static final List<String> EXAMPLES =
List.of("λx.x", "λx.λy.y x", "λx.λy.y (x x)", "let f = λx. g y y in f 3", "(λx.x x) (λx.x x)",
"(λx.λy.y (x x)) (λz. λa. z g a)");
"(λx.λy.y (x y)) (λz. λa. z g a)");
private final Paragraph instruction;
/**

7
src/main/java/edu/kit/typicalc/view/main/InputBar.java
View File

@ -1,6 +1,7 @@
package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Key;
import com.vaadin.flow.component.UI;
import com.vaadin.flow.component.button.Button;
import com.vaadin.flow.component.button.ButtonVariant;
import com.vaadin.flow.component.dependency.CssImport;
@ -81,7 +82,10 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
*/
protected void inferTerm(String term) {
inputField.setValue(term);
inferTypeButton.click();
// for some reason the Vaadin "click" does not work
//inferTypeButton.click();
UI.getCurrent().getPage().executeJs(
String.format("document.getElementById('%s').click()", INFER_BUTTON_ID));
}
private void onInputFieldValueChange() {
@ -93,6 +97,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
if (currentInput.length() < MAX_INPUT_LENGTH) {
UI.getCurrent().getPage().setTitle(getTranslation("root.typicalc") + " - " + currentInput);
callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
} else {
final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));