mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Merge branch 'master' of https://git.scc.kit.edu/pse-typinferenz/typicalc
This commit is contained in:
commit
85bf7df675
@ -4,22 +4,26 @@ function handleKey(e) {
|
|||||||
if (e.target.tagName.toLowerCase() === "vaadin-text-field") {
|
if (e.target.tagName.toLowerCase() === "vaadin-text-field") {
|
||||||
return;
|
return;
|
||||||
}
|
}
|
||||||
|
let element = null;
|
||||||
if (e.keyCode === 37) {
|
if (e.keyCode === 37) {
|
||||||
// left arrow
|
// left arrow
|
||||||
if (!e.ctrlKey) {
|
if (!e.ctrlKey) {
|
||||||
document.getElementById("previous-step").click();
|
element = document.getElementById("previous-step");
|
||||||
} else {
|
} else {
|
||||||
document.getElementById("first-step").click();
|
element = document.getElementById("first-step");
|
||||||
}
|
}
|
||||||
} else if (e.keyCode === 39) {
|
} else if (e.keyCode === 39) {
|
||||||
// right arrow
|
// right arrow
|
||||||
if (!e.ctrlKey) {
|
if (!e.ctrlKey) {
|
||||||
document.getElementById("next-step").click();
|
element = document.getElementById("next-step");
|
||||||
} else {
|
} else {
|
||||||
document.getElementById("last-step").click();
|
element = document.getElementById("last-step");
|
||||||
}
|
}
|
||||||
} else if (e.key === "/") {
|
} else if (e.key === "/") {
|
||||||
document.getElementById("inputField").focus();
|
document.getElementById("inputField").focus();
|
||||||
e.preventDefault();
|
e.preventDefault();
|
||||||
}
|
}
|
||||||
|
if (element !== null) {
|
||||||
|
element.click();
|
||||||
|
}
|
||||||
}
|
}
|
||||||
|
@ -4,6 +4,7 @@
|
|||||||
padding-right: 0;
|
padding-right: 0;
|
||||||
height: 525px;
|
height: 525px;
|
||||||
overflow-y: auto;
|
overflow-y: auto;
|
||||||
|
align-items: center;
|
||||||
}
|
}
|
||||||
|
|
||||||
#headingLayout {
|
#headingLayout {
|
||||||
|
@ -101,8 +101,8 @@ public class LatexCreator implements StepVisitor {
|
|||||||
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions());
|
String assumptions = typeAssumptionsToLatex(var.getConclusion().getTypeAssumptions());
|
||||||
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
|
String term = new LatexCreatorTerm(var.getConclusion().getLambdaTerm()).getLatex();
|
||||||
String type = generateTypeAbstraction(var.getTypeAbsInPremise());
|
String type = generateTypeAbstraction(var.getTypeAbsInPremise());
|
||||||
return DOLLAR_SIGN + PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
return PAREN_LEFT + assumptions + PAREN_RIGHT + PAREN_LEFT + term
|
||||||
+ PAREN_RIGHT + EQUALS + type + DOLLAR_SIGN;
|
+ PAREN_RIGHT + EQUALS + type;
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
||||||
@ -137,7 +137,8 @@ public class LatexCreator implements StepVisitor {
|
|||||||
@Override
|
@Override
|
||||||
public void visit(VarStepDefault varD) {
|
public void visit(VarStepDefault varD) {
|
||||||
tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC));
|
tree.insert(0, generateConclusion(varD, LABEL_VAR, UIC));
|
||||||
tree.insert(0, AXC + CURLY_LEFT + generateVarStepPremise(varD) + CURLY_RIGHT + NEW_LINE);
|
tree.insert(0, AXC + CURLY_LEFT + DOLLAR_SIGN + generateVarStepPremise(varD)
|
||||||
|
+ DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
@ -145,11 +146,11 @@ public class LatexCreator implements StepVisitor {
|
|||||||
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
||||||
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
||||||
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
||||||
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType + DOLLAR_SIGN;
|
String premiseRight = typeAbstraction + INSTANTIATE_SIGN + instantiatedType;
|
||||||
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
||||||
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
|
+ generateVarStepPremise(varL)
|
||||||
+ SPACE + LATEX_NEW_LINE + SPACE // todo less replacement fixups
|
+ SPACE + LATEX_NEW_LINE + SPACE
|
||||||
+ premiseRight.replace(DOLLAR_SIGN, "")
|
+ premiseRight
|
||||||
+ ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
|
+ ALIGN_END + DOLLAR_SIGN + CURLY_RIGHT + NEW_LINE;
|
||||||
tree.insert(0, premiseLeft);
|
tree.insert(0, premiseLeft);
|
||||||
}
|
}
|
||||||
|
@ -10,7 +10,6 @@ import com.vaadin.flow.component.html.H3;
|
|||||||
import com.vaadin.flow.component.html.Paragraph;
|
import com.vaadin.flow.component.html.Paragraph;
|
||||||
import com.vaadin.flow.component.icon.Icon;
|
import com.vaadin.flow.component.icon.Icon;
|
||||||
import com.vaadin.flow.component.icon.VaadinIcon;
|
import com.vaadin.flow.component.icon.VaadinIcon;
|
||||||
import com.vaadin.flow.component.orderedlayout.FlexComponent;
|
|
||||||
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
||||||
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
import com.vaadin.flow.component.orderedlayout.VerticalLayout;
|
||||||
import com.vaadin.flow.component.select.Select;
|
import com.vaadin.flow.component.select.Select;
|
||||||
@ -73,7 +72,6 @@ public class HelpDialog extends Dialog implements LocaleChangeObserver {
|
|||||||
typicalcInfo = new Paragraph();
|
typicalcInfo = new Paragraph();
|
||||||
typicalcInfo.setId(TYPICALC_INFO_ID);
|
typicalcInfo.setId(TYPICALC_INFO_ID);
|
||||||
contentLayout.add(typicalcInfo);
|
contentLayout.add(typicalcInfo);
|
||||||
contentLayout.setAlignItems(FlexComponent.Alignment.CENTER);
|
|
||||||
|
|
||||||
add(headingLayout, contentLayout);
|
add(headingLayout, contentLayout);
|
||||||
}
|
}
|
||||||
|
Loading…
Reference in New Issue
Block a user