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
098a358a0d
@ -5,3 +5,7 @@ vaadin-button {
|
||||
vaadin-button, iron-icon, vaadin-drawer-toggle {
|
||||
cursor: pointer;
|
||||
}
|
||||
|
||||
#closeIcon:hover {
|
||||
color: rgb(120, 120, 120);
|
||||
}
|
||||
|
3
frontend/styles/view/button-hover.css
Normal file
3
frontend/styles/view/button-hover.css
Normal file
@ -0,0 +1,3 @@
|
||||
:host(:hover)::before {
|
||||
opacity: 0.12;
|
||||
}
|
@ -15,7 +15,8 @@
|
||||
|
||||
#languageSelect {
|
||||
position: absolute;
|
||||
right: 0;
|
||||
margin: 0;
|
||||
left: 0;
|
||||
}
|
||||
|
||||
#accordion {
|
||||
|
@ -4,11 +4,13 @@ import com.vaadin.flow.component.button.Button;
|
||||
import com.vaadin.flow.component.icon.Icon;
|
||||
import com.vaadin.flow.component.icon.VaadinIcon;
|
||||
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
|
||||
/**
|
||||
* Provides a GUI in form of buttons for the user to navigate through steps.
|
||||
*/
|
||||
public class ControlPanel extends HorizontalLayout {
|
||||
public class ControlPanel extends HorizontalLayout implements LocaleChangeObserver {
|
||||
public static final String ID = "control-panel";
|
||||
|
||||
private final Button firstStep;
|
||||
@ -85,4 +87,13 @@ public class ControlPanel extends HorizontalLayout {
|
||||
public void setEnabledShareButton(boolean setEnabled) {
|
||||
share.setEnabled(setEnabled);
|
||||
}
|
||||
|
||||
@Override
|
||||
public void localeChange(LocaleChangeEvent event) {
|
||||
share.getElement().setAttribute("title", getTranslation("root.shareButtonTooltip"));
|
||||
firstStep.getElement().setAttribute("title", getTranslation("root.firstStepTooltip"));
|
||||
previousStep.getElement().setAttribute("title", getTranslation("root.previousStepTooltip"));
|
||||
nextStep.getElement().setAttribute("title", getTranslation("root.nextStepTooltip"));
|
||||
lastStep.getElement().setAttribute("title", getTranslation("root.lastStepTooltip"));
|
||||
}
|
||||
}
|
||||
|
@ -25,7 +25,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||
private static final String CLOSE_ICON_ID = "closeIcon";
|
||||
|
||||
private final TextField urlField;
|
||||
private final TextField packageField;
|
||||
private final TextArea packageArea;
|
||||
private final TextArea latexArea;
|
||||
private final H3 heading;
|
||||
|
||||
@ -34,11 +34,9 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||
* to the String that is passed as corresponding parameter.
|
||||
*
|
||||
* @param url a permalink to share with other users
|
||||
* @param latexPackages the needed LaTeX-packages to use the displayed mathematics
|
||||
* in other LaTeX documents. Should be in the form „\\usepackage<package>“
|
||||
* @param latexCode LaTeX code for users to copy into their own LaTeX document(s)
|
||||
*/
|
||||
public ShareDialog(String url, String latexPackages, String latexCode) {
|
||||
public ShareDialog(String url, String latexCode) {
|
||||
HorizontalLayout headingLayout = new HorizontalLayout();
|
||||
headingLayout.setId(HEADING_LAYOUT_ID);
|
||||
|
||||
@ -55,17 +53,17 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||
setId(SHARE_DIALOG_ID);
|
||||
|
||||
urlField = new TextField();
|
||||
packageField = new TextField();
|
||||
packageArea = new TextArea();
|
||||
latexArea = new TextArea();
|
||||
|
||||
urlField.setValue(url);
|
||||
urlField.setClassName(FIELD_CLASS);
|
||||
packageField.setValue(latexPackages);
|
||||
packageField.setClassName(FIELD_CLASS);
|
||||
packageArea.setValue(getTranslation("share.neededPackages"));
|
||||
packageArea.setClassName(FIELD_CLASS);
|
||||
latexArea.setValue(latexCode);
|
||||
latexArea.setClassName(FIELD_CLASS);
|
||||
|
||||
layout.add(urlField, packageField, latexArea);
|
||||
layout.add(urlField, packageArea, latexArea);
|
||||
|
||||
add(headingLayout, layout);
|
||||
}
|
||||
@ -75,7 +73,7 @@ public class ShareDialog extends Dialog implements LocaleChangeObserver {
|
||||
public void localeChange(LocaleChangeEvent localeChangeEvent) {
|
||||
heading.setText(getTranslation("share.heading"));
|
||||
urlField.setLabel(getTranslation("share.url.label"));
|
||||
packageField.setLabel(getTranslation("share.packages.label"));
|
||||
packageArea.setLabel(getTranslation("share.packages.label"));
|
||||
latexArea.setLabel(getTranslation("share.latex.label"));
|
||||
}
|
||||
}
|
||||
|
@ -82,7 +82,7 @@ public class TypeInferenceView extends VerticalLayout
|
||||
@Override
|
||||
public void shareButton() {
|
||||
UI.getCurrent().getPage().executeJs("return decodeURI(window.location.href)").then(url ->
|
||||
new ShareDialog(url.asString(), lc.getLatexPackages(), lc.getTree()).open()
|
||||
new ShareDialog(url.asString(), lc.getTree()).open()
|
||||
);
|
||||
}
|
||||
|
||||
|
@ -77,16 +77,6 @@ public class LatexCreator implements StepVisitor {
|
||||
return constraintsCreator.getTreeNumbers();
|
||||
}
|
||||
|
||||
/**
|
||||
* Returns needed LaTeX packages
|
||||
*
|
||||
* @return the packages needed for the LaTeX-code from getTree() to work
|
||||
*/
|
||||
public String getLatexPackages() {
|
||||
return BUSSPROOFS;
|
||||
}
|
||||
|
||||
|
||||
private String conclusionToLatex(Conclusion conclusion) {
|
||||
String typeAssumptions = typeAssumptionsToLatex(conclusion.getTypeAssumptions());
|
||||
String term = new LatexCreatorTerm(conclusion.getLambdaTerm()).getLatex();
|
||||
@ -155,8 +145,7 @@ public class LatexCreator implements StepVisitor {
|
||||
tree.insert(0, generateConclusion(varL, LABEL_VAR, UIC));
|
||||
String typeAbstraction = generateTypeAbstraction(varL.getTypeAbsInPremise());
|
||||
String instantiatedType = new LatexCreatorType(varL.getInstantiatedTypeAbs()).getLatex();
|
||||
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType
|
||||
+ DOLLAR_SIGN + NEW_LINE;
|
||||
String premiseRight = DOLLAR_SIGN + typeAbstraction + INSTANTIATE_SIGN + instantiatedType + DOLLAR_SIGN;
|
||||
String premiseLeft = AXC + CURLY_LEFT + DOLLAR_SIGN + ALIGN_BEGIN
|
||||
+ generateVarStepPremise(varL).replace(DOLLAR_SIGN, "")
|
||||
+ SPACE + LATEX_NEW_LINE + SPACE // todo less replacement fixups
|
||||
|
@ -74,6 +74,4 @@ public final class LatexCreatorConstants {
|
||||
protected static final String ALIGN_END = "\\end{aligned}";
|
||||
protected static final String SPLIT_BEGIN = "\\begin{split}";
|
||||
protected static final String SPLIT_END = "\\end{split}";
|
||||
|
||||
protected static final String BUSSPROOFS = "\\usepackage{bussproofs}";
|
||||
}
|
||||
|
@ -71,6 +71,7 @@ public class InferenceRuleField extends VerticalLayout implements LocaleChangeOb
|
||||
@Override
|
||||
public void localeChange(LocaleChangeEvent event) {
|
||||
ruleName.setText(getTranslation(nameKey));
|
||||
copyButton.getElement().setAttribute("title", getTranslation("root.copyLatexTooltip"));
|
||||
}
|
||||
|
||||
}
|
||||
|
@ -35,12 +35,15 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
private static final String INFER_BUTTON_ID = "inferButton";
|
||||
private static final String EXAMPLE_BUTTON_ID = "exampleButton";
|
||||
private static final String LAMBDA_BUTTON_ID = "lambdaButton";
|
||||
private static final String ASS_BUTTON_ID = "assButton";
|
||||
|
||||
private static final short MAX_INPUT_LENGTH = 1000;
|
||||
|
||||
private final transient Consumer<Pair<String, Map<String, String>>> callback;
|
||||
private final Button infoIcon;
|
||||
private final TextField inputField;
|
||||
private TypeAssumptionsArea typeAssumptionsArea;
|
||||
private final Button exampleButton;
|
||||
private final Button inferTypeButton;
|
||||
private final Button typeAssumptions;
|
||||
|
||||
@ -53,7 +56,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
protected InputBar(Consumer<Pair<String, Map<String, String>>> callback) {
|
||||
this.callback = callback;
|
||||
|
||||
Button infoIcon = new Button(new Icon(VaadinIcon.INFO_CIRCLE));
|
||||
infoIcon = new Button(new Icon(VaadinIcon.INFO_CIRCLE));
|
||||
infoIcon.addClickListener(event -> onInfoIconClick());
|
||||
|
||||
inputField = new TextField();
|
||||
@ -78,8 +81,9 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
lambdaButton.setId(LAMBDA_BUTTON_ID);
|
||||
UI.getCurrent().getPage().executeJs("window.lambdaButtonListener($0, $1);", LAMBDA_BUTTON_ID, INPUT_FIELD_ID);
|
||||
typeAssumptions = new Button("", event -> onTypeAssumptionsButton());
|
||||
typeAssumptions.setId(ASS_BUTTON_ID);
|
||||
typeAssumptionsArea = new TypeAssumptionsArea();
|
||||
Button exampleButton = new Button(VaadinIcon.PAPERCLIP.create(), event -> onExampleButtonClick());
|
||||
exampleButton = new Button(VaadinIcon.PAPERCLIP.create(), event -> onExampleButtonClick());
|
||||
exampleButton.setId(EXAMPLE_BUTTON_ID);
|
||||
inferTypeButton = new Button("", event -> onTypeInferButtonClick());
|
||||
inferTypeButton.addClickShortcut(Key.ENTER).listenOn(this);
|
||||
@ -138,5 +142,7 @@ public class InputBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
inputField.setPlaceholder(getTranslation("root.inputFieldPlaceholder"));
|
||||
inferTypeButton.setText(getTranslation("root.typeInfer"));
|
||||
typeAssumptions.setText(getTranslation("root.typeAssumptions"));
|
||||
infoIcon.getElement().setAttribute("title", getTranslation("root.inputSyntax"));
|
||||
exampleButton.getElement().setAttribute("title", getTranslation("root.exampleTooltip"));
|
||||
}
|
||||
}
|
||||
|
@ -9,6 +9,9 @@ import com.vaadin.flow.component.html.H1;
|
||||
import com.vaadin.flow.component.icon.Icon;
|
||||
import com.vaadin.flow.component.icon.VaadinIcon;
|
||||
import com.vaadin.flow.component.orderedlayout.HorizontalLayout;
|
||||
import com.vaadin.flow.i18n.LocaleChangeEvent;
|
||||
import com.vaadin.flow.i18n.LocaleChangeObserver;
|
||||
|
||||
import edu.kit.typicalc.view.main.MainView.MainViewListener;
|
||||
import org.apache.commons.lang3.tuple.Pair;
|
||||
|
||||
@ -20,7 +23,9 @@ import java.util.function.Consumer;
|
||||
* Contains all the components constantly shown in the upper part of the webpage.
|
||||
*/
|
||||
@CssImport("./styles/view/main/upper-bar.css")
|
||||
public class UpperBar extends HorizontalLayout {
|
||||
@CssImport(value = "./styles/view/button-hover.css", themeFor = "vaadin-button")
|
||||
@CssImport(value = "./styles/view/button-hover.css", themeFor = "vaadin-drawer-toggle")
|
||||
public class UpperBar extends HorizontalLayout implements LocaleChangeObserver {
|
||||
private static final long serialVersionUID = -7344967027514015830L;
|
||||
|
||||
/*
|
||||
@ -32,6 +37,8 @@ public class UpperBar extends HorizontalLayout {
|
||||
private static final String UPPER_BAR_ID = "header";
|
||||
|
||||
private final InputBar inputBar;
|
||||
private final Button toggle;
|
||||
private final Button helpButton;
|
||||
|
||||
private final transient MainViewListener presenter;
|
||||
private final transient Consumer<Pair<String, Map<String, String>>> setTermInURL;
|
||||
@ -47,15 +54,16 @@ public class UpperBar extends HorizontalLayout {
|
||||
this.presenter = presenter;
|
||||
this.setTermInURL = setTermInURL;
|
||||
|
||||
toggle = new DrawerToggle();
|
||||
H1 viewTitle = new H1(new Anchor("/", getTranslation("root.typicalc")));
|
||||
viewTitle.setId(VIEW_TITLE_ID);
|
||||
this.inputBar = new InputBar(this::typeInfer);
|
||||
inputBar.setId(INPUT_BAR_ID);
|
||||
Button helpIcon = new Button(new Icon(VaadinIcon.QUESTION_CIRCLE));
|
||||
helpIcon.addClickListener(event -> onHelpIconClick());
|
||||
helpIcon.setId(HELP_ICON_ID);
|
||||
helpButton = new Button(new Icon(VaadinIcon.QUESTION_CIRCLE));
|
||||
helpButton.addClickListener(event -> onHelpIconClick());
|
||||
helpButton.setId(HELP_ICON_ID);
|
||||
|
||||
add(new DrawerToggle(), viewTitle, inputBar, helpIcon);
|
||||
add(toggle, viewTitle, inputBar, helpButton);
|
||||
setId(UPPER_BAR_ID);
|
||||
getThemeList().set("dark", true);
|
||||
setSpacing(false);
|
||||
@ -94,4 +102,10 @@ public class UpperBar extends HorizontalLayout {
|
||||
Dialog helpDialog = new HelpDialog();
|
||||
helpDialog.open();
|
||||
}
|
||||
|
||||
@Override
|
||||
public void localeChange(LocaleChangeEvent event) {
|
||||
toggle.getElement().setAttribute("title", getTranslation("root.drawerToggleTooltip"));
|
||||
helpButton.getElement().setAttribute("title", getTranslation("root.helpIconTooltip"));
|
||||
}
|
||||
}
|
||||
|
@ -80,3 +80,7 @@ root.varLetLatex=\
|
||||
\\LeftLabel{\\textrm V{\\small AR}}\
|
||||
\\BinaryInfC{$\\Gamma \\vdash \\texttt{x} : \\tau$}\
|
||||
\\end{prooftree}
|
||||
|
||||
share.neededPackages=\
|
||||
\\usepackage{bussproofs}\n\
|
||||
\\usepackage{amsmath}
|
@ -107,6 +107,15 @@ root.text7=Der Teilen-Knopfs wird betätigt, um das entsprechende Dialogfenster
|
||||
root.image8=/carousel/UseExportDialog.png
|
||||
root.text8=In dem Dialogfenster sind der Permalink zur aktuellen Seite, der Latex-Code des Baums und die im Code \
|
||||
verwendeten Pakete aufgelistet.
|
||||
root.copyLatexTooltip=Kopiere LaTeX-code
|
||||
root.drawerToggleTooltip=Ableitungsregeln
|
||||
root.helpIconTooltip=Hilfe und Sprachwechsel
|
||||
root.exampleTooltip=Beispielterme
|
||||
root.shareButtonTooltip=LaTeX-Code und Permalink
|
||||
root.lastStepTooltip=Letzter Schritt
|
||||
root.firstStepTooltip=Erster Schritt
|
||||
root.previousStepTooltip=Vorheriger Schritt
|
||||
root.nextStepTooltip=Nächster Schritt
|
||||
|
||||
root.absLetLatex=\
|
||||
\\begin{prooftree}\
|
||||
|
@ -100,6 +100,15 @@ root.text7=The share button is clicked to open up the corresponding dialog.
|
||||
root.image8=/carousel/UseExportDialog.png
|
||||
root.text8=The dialog contains a permalink to the current page, the LaTeX-code of the tree and the packages needed \
|
||||
to compile the code.
|
||||
root.copyLatexTooltip=Copy LaTeX code
|
||||
root.drawerToggleTooltip=Type inference rules
|
||||
root.helpIconTooltip=Help and language switch
|
||||
root.exampleTooltip=Example terms
|
||||
root.shareButtonTooltip=LaTeX code and permalink
|
||||
root.lastStepTooltip=Last step
|
||||
root.firstStepTooltip=First step
|
||||
root.previousStepTooltip=Previous step
|
||||
root.nextStepTooltip=Next step
|
||||
|
||||
root.absLetLatex=\
|
||||
\\begin{prooftree}\
|
||||
|
@ -47,7 +47,7 @@ public class InputBarElement extends HorizontalLayoutElement {
|
||||
* Opens the type assumptions area.
|
||||
*/
|
||||
public void openTypeAssumptionsArea() {
|
||||
$(ButtonElement.class).first().click();
|
||||
$(ButtonElement.class).id("assButton").click();
|
||||
}
|
||||
|
||||
}
|
||||
|
Loading…
Reference in New Issue
Block a user