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

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

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

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

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

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

@ -1,6 +1,7 @@
package edu.kit.typicalc.view.main; package edu.kit.typicalc.view.main;
import com.vaadin.flow.component.Key; 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.Button;
import com.vaadin.flow.component.button.ButtonVariant; import com.vaadin.flow.component.button.ButtonVariant;
import com.vaadin.flow.component.dependency.CssImport; import com.vaadin.flow.component.dependency.CssImport;
@ -81,7 +82,10 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
*/ */
protected void inferTerm(String term) { protected void inferTerm(String term) {
inputField.setValue(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() { private void onInputFieldValueChange() {
@ -93,6 +97,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY); String currentInput = inputField.getOptionalValue().orElse(StringUtils.EMPTY);
if (currentInput.length() < MAX_INPUT_LENGTH) { if (currentInput.length() < MAX_INPUT_LENGTH) {
UI.getCurrent().getPage().setTitle(getTranslation("root.typicalc") + " - " + currentInput);
callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions())); callback.accept(Pair.of(currentInput, typeAssumptionsArea.getTypeAssumptions()));
} else { } else {
final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput")); final Notification errorNotification = new ErrorNotification(getTranslation("root.overlongInput"));