mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-09-18 17:55:14 +00:00
Fixups for newer versions
This commit is contained in:
parent
dc9d6c046b
commit
b09ba5a83a
2
.gitignore
vendored
2
.gitignore
vendored
@ -23,3 +23,5 @@ webpack.generated.js
|
|||||||
|
|
||||||
/fuzz-results
|
/fuzz-results
|
||||||
/.npmrc
|
/.npmrc
|
||||||
|
|
||||||
|
/src/main/dev-bundle/
|
||||||
|
@ -14,7 +14,7 @@ window.buttonListener = (buttonID: string, inputID: string) => {
|
|||||||
const button = document.getElementById(buttonID)!;
|
const button = document.getElementById(buttonID)!;
|
||||||
const input = document.getElementById(inputID)!;
|
const input = document.getElementById(inputID)!;
|
||||||
button.addEventListener('click', () => {
|
button.addEventListener('click', () => {
|
||||||
const area = input.shadowRoot!.querySelector('input')!;
|
const area = input as HTMLInputElement;
|
||||||
let start = area.selectionStart!;
|
let start = area.selectionStart!;
|
||||||
area.value = [area.value.slice(0, start), replacement, area.value.slice(start)].join('');
|
area.value = [area.value.slice(0, start), replacement, area.value.slice(start)].join('');
|
||||||
area.selectionStart = ++start;
|
area.selectionStart = ++start;
|
||||||
@ -30,7 +30,7 @@ window.characterListener = (inputID: string) => {
|
|||||||
let toReplace = (inputID === "term-input-field") ? '\\' : '!';
|
let toReplace = (inputID === "term-input-field") ? '\\' : '!';
|
||||||
let replacement = (inputID === "term-input-field") ? 'λ' : '∀';
|
let replacement = (inputID === "term-input-field") ? 'λ' : '∀';
|
||||||
document.getElementById(inputID)!.addEventListener('keyup', e => {
|
document.getElementById(inputID)!.addEventListener('keyup', e => {
|
||||||
const area = (e.target as HTMLElement).shadowRoot!.querySelector('input')!;
|
const area = (e.target as HTMLInputElement)!;
|
||||||
if (area.value.indexOf(toReplace) >= 0) {
|
if (area.value.indexOf(toReplace) >= 0) {
|
||||||
const start = area.selectionStart;
|
const start = area.selectionStart;
|
||||||
const end = area.selectionEnd;
|
const end = area.selectionEnd;
|
||||||
|
@ -4,7 +4,7 @@ window.autoSelect = (className: string) => {
|
|||||||
let el = document.getElementsByClassName(className);
|
let el = document.getElementsByClassName(className);
|
||||||
Array.from(el).forEach(field => {
|
Array.from(el).forEach(field => {
|
||||||
field.addEventListener('focus', event => {
|
field.addEventListener('focus', event => {
|
||||||
const root = (event.target! as HTMLElement).shadowRoot!;
|
const root = (event.target! as HTMLElement);
|
||||||
let e: HTMLInputElement | HTMLTextAreaElement | null
|
let e: HTMLInputElement | HTMLTextAreaElement | null
|
||||||
= root.querySelector<HTMLInputElement>('input');
|
= root.querySelector<HTMLInputElement>('input');
|
||||||
if (!e) {
|
if (!e) {
|
||||||
|
6
frontend/src/svg-pan-zoom.min.js
vendored
6
frontend/src/svg-pan-zoom.min.js
vendored
File diff suppressed because one or more lines are too long
@ -7,7 +7,7 @@ window.addTypeInputListener = (className: string) => {
|
|||||||
const el = document.getElementsByClassName(className);
|
const el = document.getElementsByClassName(className);
|
||||||
if (el) {
|
if (el) {
|
||||||
const listener = (e: Event) => {
|
const listener = (e: Event) => {
|
||||||
const area = (e.target! as HTMLElement).shadowRoot!.querySelector<HTMLInputElement>('input');
|
const area = e.target! as HTMLInputElement;
|
||||||
modifyValue(area!);
|
modifyValue(area!);
|
||||||
};
|
};
|
||||||
Array.from(el).forEach(function (element) {
|
Array.from(el).forEach(function (element) {
|
||||||
|
14488
package-lock.json
generated
Normal file
14488
package-lock.json
generated
Normal file
File diff suppressed because it is too large
Load Diff
@ -26,6 +26,7 @@ public class Application extends SpringBootServletInitializer
|
|||||||
* @param args empty array
|
* @param args empty array
|
||||||
*/
|
*/
|
||||||
public static void main(String[] args) {
|
public static void main(String[] args) {
|
||||||
|
System.setProperty("user.home", "/home/arne/.cache");
|
||||||
LaunchUtil.launchBrowserInDevelopmentMode(SpringApplication.run(Application.class, args));
|
LaunchUtil.launchBrowserInDevelopmentMode(SpringApplication.run(Application.class, args));
|
||||||
}
|
}
|
||||||
|
|
||||||
|
@ -12,10 +12,10 @@ import edu.kit.typicalc.presenter.Presenter;
|
|||||||
import edu.kit.typicalc.view.content.errorcontent.ErrorView;
|
import edu.kit.typicalc.view.content.errorcontent.ErrorView;
|
||||||
import edu.kit.typicalc.view.content.infocontent.StartPageView;
|
import edu.kit.typicalc.view.content.infocontent.StartPageView;
|
||||||
import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
|
import edu.kit.typicalc.view.content.typeinferencecontent.TypeInferenceView;
|
||||||
|
import jakarta.servlet.http.HttpServletResponse;
|
||||||
import org.apache.commons.lang3.StringUtils;
|
import org.apache.commons.lang3.StringUtils;
|
||||||
import org.apache.commons.lang3.tuple.Pair;
|
import org.apache.commons.lang3.tuple.Pair;
|
||||||
|
|
||||||
import javax.servlet.http.HttpServletResponse;
|
|
||||||
import java.net.URLDecoder;
|
import java.net.URLDecoder;
|
||||||
import java.net.URLEncoder;
|
import java.net.URLEncoder;
|
||||||
import java.nio.charset.StandardCharsets;
|
import java.nio.charset.StandardCharsets;
|
||||||
|
@ -69,10 +69,10 @@ public class UpperBar extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
helpButton.setId(HELP_ICON_ID);
|
helpButton.setId(HELP_ICON_ID);
|
||||||
|
|
||||||
renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase());
|
renderer = item -> getTranslation("root." + item.getDisplayLanguage(Locale.ENGLISH).toLowerCase());
|
||||||
languageSelect = new Select<>(Locale.GERMAN, Locale.ENGLISH);
|
languageSelect = new Select<>("",
|
||||||
|
event -> UI.getCurrent().getSession().setLocale(event.getValue()), Locale.GERMAN, Locale.ENGLISH);
|
||||||
languageSelect.setTextRenderer(renderer);
|
languageSelect.setTextRenderer(renderer);
|
||||||
languageSelect.setValue(UI.getCurrent().getLocale());
|
languageSelect.setValue(UI.getCurrent().getLocale());
|
||||||
languageSelect.addValueChangeListener(event -> UI.getCurrent().getSession().setLocale(event.getValue()));
|
|
||||||
languageSelect.setId(LANGUAGE_SELECT_ID);
|
languageSelect.setId(LANGUAGE_SELECT_ID);
|
||||||
HorizontalLayout topLine = new HorizontalLayout(languageSelect, viewTitle, helpButton);
|
HorizontalLayout topLine = new HorizontalLayout(languageSelect, viewTitle, helpButton);
|
||||||
topLine.setId(TOP_LINE_ID);
|
topLine.setId(TOP_LINE_ID);
|
||||||
|
Loading…
Reference in New Issue
Block a user