mirror of
https://gitlab.kit.edu/uskyk/typicalc.git
synced 2024-11-08 18:30:42 +00:00
Removed unnecessary information in error
changed spacing in error message "Term" instead of "Input"
This commit is contained in:
parent
3477bff512
commit
fea2b7035a
@ -61,19 +61,17 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
case UNEXPECTED_TOKEN:
|
case UNEXPECTED_TOKEN:
|
||||||
Optional<Token> cause = error.getCause();
|
Optional<Token> cause = error.getCause();
|
||||||
if (cause.isPresent()) {
|
if (cause.isPresent()) {
|
||||||
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term)));
|
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term
|
||||||
additionalInformation.add(
|
+ "\n" + " ".repeat(Math.max(getTranslation("root.termForError").length(),
|
||||||
new Span(new Pre(" ".repeat(Math.max(getTranslation("root.termForError").length(),
|
cause.get().getPos() + getTranslation("root.termForError").length()))
|
||||||
cause.get().getPos() + getTranslation("root.termForError").length()))
|
|
||||||
+ "^ " + getTranslation("root.wrongCharacter") + cause.get().getText())));
|
+ "^ " + getTranslation("root.wrongCharacter") + cause.get().getText())));
|
||||||
}
|
}
|
||||||
break;
|
break;
|
||||||
case UNEXPECTED_CHARACTER:
|
case UNEXPECTED_CHARACTER:
|
||||||
char c = error.getWrongCharacter();
|
char c = error.getWrongCharacter();
|
||||||
if (c != '\0') {
|
if (c != '\0') {
|
||||||
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term)));
|
additionalInformation.add(new Span(new Pre(getTranslation("root.termForError") + term
|
||||||
additionalInformation.add(new Span(
|
+ "\n" + " ".repeat(Math.max(getTranslation("root.termForError").length(),
|
||||||
new Pre(" ".repeat(Math.max(getTranslation("root.termForError").length(),
|
|
||||||
error.getPosition() + getTranslation("root.termForError").length()))
|
error.getPosition() + getTranslation("root.termForError").length()))
|
||||||
+ "^ " + getTranslation("root.wrongCharacter") + c)));
|
+ "^ " + getTranslation("root.wrongCharacter") + c)));
|
||||||
} else {
|
} else {
|
||||||
@ -107,7 +105,7 @@ public class ErrorView extends VerticalLayout implements LocaleChangeObserver {
|
|||||||
getTranslation("error.expectedToken", correct))));
|
getTranslation("error.expectedToken", correct))));
|
||||||
}
|
}
|
||||||
|
|
||||||
return new Div(summary, additionalInformation);
|
return new Div(additionalInformation);
|
||||||
}
|
}
|
||||||
|
|
||||||
@Override
|
@Override
|
||||||
|
@ -106,7 +106,7 @@ root.tooFewTokensHelp=Überprüfe, ob alle Let-, Abs- und App-Terme über die n
|
|||||||
root.UNEXPECTED_TOKEN=Die Eingabe entspricht nicht der im Info-Dialog spezifizierten Syntax!
|
root.UNEXPECTED_TOKEN=Die Eingabe entspricht nicht der im Info-Dialog spezifizierten Syntax!
|
||||||
root.UNEXPECTED_CHARACTER=Die Eingabe enthält ein Zeichen, welches an dieser Stelle nicht erlaubt ist!
|
root.UNEXPECTED_CHARACTER=Die Eingabe enthält ein Zeichen, welches an dieser Stelle nicht erlaubt ist!
|
||||||
error.heading=Syntaktisch falsche Eingabe!
|
error.heading=Syntaktisch falsche Eingabe!
|
||||||
root.termForError=Eingabe:\u0020
|
root.termForError=Term:\u0020
|
||||||
root.wrongCharacter=Falsches Zeichen:\u0020
|
root.wrongCharacter=Falsches Zeichen:\u0020
|
||||||
error.expectedToken=Erwartet: {0}
|
error.expectedToken=Erwartet: {0}
|
||||||
error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \
|
error.hint=Die Grammatiken, die die korrekte Syntax eines Terms und der Typannahmen beschreiben, \
|
||||||
|
@ -100,7 +100,7 @@ root.UNEXPECTED_TOKEN=The input does not match the syntax specified in the info
|
|||||||
root.UNEXPECTED_CHARACTER=The input contains a character which is not allowed at this position.
|
root.UNEXPECTED_CHARACTER=The input contains a character which is not allowed at this position.
|
||||||
error.heading=Input is syntactically wrong!
|
error.heading=Input is syntactically wrong!
|
||||||
root.wrongCharacter=Wrong character:\u0020
|
root.wrongCharacter=Wrong character:\u0020
|
||||||
root.termForError=Input:\u0020
|
root.termForError=Term:\u0020
|
||||||
error.expectedToken=Expected: {0}
|
error.expectedToken=Expected: {0}
|
||||||
error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \
|
error.hint=The grammars describing the correct syntax of a term or a type assumption can also be reached \
|
||||||
via the info icon.
|
via the info icon.
|
||||||
|
Loading…
Reference in New Issue
Block a user