Set page title to lambda term

This commit is contained in:
Arne Keller 2021-02-06 10:57:35 +01:00
parent 843430439d
commit d3fd5b99a8
2 changed files with 4 additions and 3 deletions

View File

@ -171,9 +171,9 @@ class MathjaxProofTree extends MathjaxAdapter {
i += 1;
}
}
// 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);
// 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

View File

@ -97,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"));