From cb55a9c0f2eaaa102ae5c2e5be05df27c1deb49c Mon Sep 17 00:00:00 2001 From: dgelessus <dgelessus@users.noreply.github.com> Date: Mon, 2 Jul 2018 16:32:25 +0200 Subject: [PATCH] Add highlighting for errors with locations (closes #19) This works for ProBErrors that include location information, which are currently only type errors. (Parse errors are wrapped in ProBErrors, but do not include proper location information.) --- notebooks/tests/load_cell.ipynb | 89 +++++++++++++++++++ .../java/de/prob2/jupyter/ProBKernel.java | 65 ++++++++++++-- .../prob2/jupyter/commands/AssertCommand.java | 2 +- .../prob2/jupyter/commands/CommandUtils.java | 17 ++++ .../de/prob2/jupyter/commands/DotCommand.java | 4 +- .../prob2/jupyter/commands/EvalCommand.java | 2 +- .../jupyter/commands/LoadCellCommand.java | 4 +- .../jupyter/commands/PrettyPrintCommand.java | 2 +- .../prob2/jupyter/commands/SolveCommand.java | 3 +- .../prob2/jupyter/commands/TableCommand.java | 2 +- .../prob2/jupyter/commands/TypeCommand.java | 2 +- .../commands/WithSourceCodeException.java | 26 ++++++ 12 files changed, 205 insertions(+), 13 deletions(-) create mode 100644 src/main/java/de/prob2/jupyter/commands/WithSourceCodeException.java diff --git a/notebooks/tests/load_cell.ipynb b/notebooks/tests/load_cell.ipynb index 26d949f..20c55c7 100644 --- a/notebooks/tests/load_cell.ipynb +++ b/notebooks/tests/load_cell.ipynb @@ -149,6 +149,95 @@ "source": [ "MININT..MAXINT" ] + }, + { + "cell_type": "markdown", + "metadata": {}, + "source": [ + "Syntax and type errors are displayed." + ] + }, + { + "cell_type": "code", + "execution_count": 6, + "metadata": {}, + "outputs": [ + { + "ename": "WithSourceCodeException", + "evalue": "de.prob.exception.ProBError: ProB returned error messages:\nError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES'", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mnull\u001b[0m", + "\u001b[1m\u001b[31mError: [1,20] expecting: 'ABSTRACT_CONSTANTS', 'ABSTRACT_VARIABLES', 'ASSERTIONS', 'CONCRETE_CONSTANTS', 'CONCRETE_VARIABLES', 'CONSTANTS', 'CONSTRAINTS', 'DEFINITIONS', 'EXPRESSIONS', 'PREDICATES', 'END', 'EXTENDS', 'IMPORTS', 'INCLUDES', initialisation, 'INVARIANT', 'LOCAL_OPERATIONS', operations, 'PROMOTES', 'PROPERTIES', 'SEES', 'SETS', 'USES', 'VALUES', 'VARIABLES', 'FREETYPES', 'REFERENCES'\u001b[0m" + ] + } + ], + "source": [ + "::load\n", + "MACHINE syntaxerror" + ] + }, + { + "cell_type": "code", + "execution_count": 7, + "metadata": { + "scrolled": true + }, + "outputs": [ + { + "ename": "WithSourceCodeException", + "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\nError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m", + "\u001b[1m\u001b[30m2 errors:\u001b[0m", + "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\u001b[0m", + "\u001b[1m\u001b[31mError end column 19 out of bounds (0..18)\u001b[0m", + "\u001b[1m\u001b[31mError: Identifier 'x' declared twice at (Line:Col[:File]) (Line:2 Col:17) and (Line:2 Col:14) (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:17 to 2:19)\u001b[0m", + "\u001b[1m\u001b[31mError end column 19 out of bounds (0..18)\u001b[0m" + ] + } + ], + "source": [ + "::load\n", + "MACHINE duplicate\n", + " CONSTANTS x, x\n", + " PROPERTIES x : INT\n", + "END" + ] + }, + { + "cell_type": "code", + "execution_count": 8, + "metadata": {}, + "outputs": [ + { + "ename": "WithSourceCodeException", + "evalue": "de.prob.exception.ProBError: Prolog said no.\nProB returned error messages:\nError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:16)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:17)\nError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:26)", + "output_type": "error", + "traceback": [ + "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mProlog said no.\u001b[0m", + "\u001b[1m\u001b[30m3 errors:\u001b[0m", + "\u001b[1m\u001b[31mError: Could not infer type of x (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:2:14 to 2:16)\u001b[0m", + "\u001b[1m\u001b[31mError end column 16 out of bounds (0..15)\u001b[0m", + "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\" ^ \"string\" ^ \"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:35 to 5:17)\u001b[0m", + "\u001b[1m\u001b[30m PROPERTIES 1 = \"string\" & 1 = (\u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\"\u001b[0m", + "\u001b[1m\u001b[30m\u001b[41m ^ \"string\"\u001b[0m", + "\u001b[1m\u001b[30m\u001b[41m ^ \"string\u001b[0m\u001b[1m\u001b[30m\")\u001b[0m", + "\u001b[1m\u001b[31mError: Type mismatch: Expected INTEGER, but was STRING in '\"string\"' (/Users/Shared/Uni/SHK/ProB2/prob2-jupyter-kernel/notebooks/tests/(machine from Jupyter cell).mch:3:19 to 3:26)\u001b[0m", + "\u001b[1m\u001b[30m PROPERTIES 1 = \u001b[0m\u001b[1m\u001b[30m\u001b[41m\"string\u001b[0m\u001b[1m\u001b[30m\" & 1 = (\"string\"\u001b[0m" + ] + } + ], + "source": [ + "::load\n", + "MACHINE typeerrors\n", + " CONSTANTS x\n", + " PROPERTIES 1 = \"string\" & 1 = (\"string\"\n", + " ^ \"string\"\n", + " ^ \"string\")\n", + "END" + ] } ], "metadata": { diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java index 04add0d..0dbb6e4 100644 --- a/src/main/java/de/prob2/jupyter/ProBKernel.java +++ b/src/main/java/de/prob2/jupyter/ProBKernel.java @@ -46,6 +46,7 @@ import de.prob2.jupyter.commands.TimeCommand; import de.prob2.jupyter.commands.TraceCommand; import de.prob2.jupyter.commands.TypeCommand; import de.prob2.jupyter.commands.VersionCommand; +import de.prob2.jupyter.commands.WithSourceCodeException; import io.github.spencerpark.jupyter.kernel.BaseKernel; import io.github.spencerpark.jupyter.kernel.LanguageInfo; @@ -306,13 +307,64 @@ public final class ProBKernel extends BaseKernel { this.animationSelector.getCurrentTrace().getStateSpace().kill(); } + private @NotNull List<@NotNull String> formatErrorSource(final @NotNull List<@NotNull String> sourceLines, final @NotNull ErrorItem.Location location) { + final List<String> out = new ArrayList<>(); + if (location.getStartLine() < 1 || location.getStartLine() >= sourceLines.size()) { + out.add(this.errorStyler.secondary(String.format("Error start line %d out of bounds (1..%d)", location.getStartLine(), sourceLines.size()+1))); + return out; + } + if (location.getEndLine() < 1 || location.getEndLine() >= sourceLines.size()) { + out.add(this.errorStyler.secondary(String.format("Error end line %d out of bounds (1..%d)", location.getEndLine(), sourceLines.size()+1))); + return out; + } + final List<String> errorLines = sourceLines.subList(location.getStartLine()-1, location.getEndLine()); + assert !errorLines.isEmpty(); + final String firstLine = errorLines.get(0); + final String lastLine = errorLines.get(errorLines.size() - 1); + if (location.getStartColumn() < 0 || location.getStartColumn() > firstLine.length()) { + out.add(this.errorStyler.secondary(String.format("Error start column %d out of bounds (0..%d)", location.getStartColumn(), firstLine.length()))); + return out; + } + if (location.getEndColumn() < 0 || location.getEndColumn() > lastLine.length()) { + out.add(this.errorStyler.secondary(String.format("Error end column %d out of bounds (0..%d)", location.getEndColumn(), lastLine.length()))); + return out; + } + if (errorLines.size() == 1) { + out.add( + this.errorStyler.primary(firstLine.substring(0, location.getStartColumn())) + + this.errorStyler.highlight(firstLine.substring(location.getStartColumn(), location.getEndColumn())) + + this.errorStyler.primary(firstLine.substring(location.getEndColumn())) + ); + } else { + out.add( + this.errorStyler.primary(firstLine.substring(0, location.getStartColumn())) + + this.errorStyler.highlight(firstLine.substring(location.getStartColumn())) + ); + errorLines.subList(1, errorLines.size()-1).stream().map(this.errorStyler::highlight).collect(Collectors.toCollection(() -> out)); + out.add( + this.errorStyler.highlight(lastLine.substring(0, location.getEndColumn())) + + this.errorStyler.primary(lastLine.substring(location.getEndColumn())) + ); + } + return out; + } + @Override public @NotNull List<@NotNull String> formatError(final Exception e) { try { + LOGGER.warn("Exception while executing command from user", e); if (e instanceof UserErrorException) { return this.errorStyler.secondaryLines(String.valueOf(e.getMessage())); - } else if (e instanceof ProBError) { - final ProBError proBError = (ProBError)e; + } else if (e instanceof ProBError || e instanceof WithSourceCodeException) { + final List<String> sourceLines; + final ProBError proBError; + if (e instanceof WithSourceCodeException) { + sourceLines = Arrays.asList(((WithSourceCodeException)e).getSourceCode().split("\n")); + proBError = ((WithSourceCodeException)e).getCause(); + } else { + sourceLines = Collections.emptyList(); + proBError = (ProBError)e; + } final List<String> out = new ArrayList<>(Arrays.asList(( this.errorStyler.primary("Error from ProB: ") + this.errorStyler.secondary(String.valueOf(proBError.getOriginalMessage())) @@ -322,12 +374,15 @@ public final class ProBKernel extends BaseKernel { // (This matches the normal behavior of ProBError.) } else if (proBError.getErrors().isEmpty()) { out.addAll(this.errorStyler.primaryLines("ProB returned no error messages.\n")); - } else if (proBError.getErrors().size() == 1) { - out.addAll(this.errorStyler.secondaryLines(proBError.getErrors().get(0).toString())); } else { - out.addAll(this.errorStyler.primaryLines(proBError.getErrors().size() + " errors:\n")); + if (proBError.getErrors().size() > 1) { + out.addAll(this.errorStyler.primaryLines(proBError.getErrors().size() + " errors:\n")); + } for (final ErrorItem error : proBError.getErrors()) { out.addAll(this.errorStyler.secondaryLines(error.toString())); + for (final ErrorItem.Location location : error.getLocations()) { + out.addAll(formatErrorSource(sourceLines, location)); + } } } return out; diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java index 40c2699..b77cb0c 100644 --- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java @@ -43,7 +43,7 @@ public final class AssertCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { - final AbstractEvalResult result = this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE); + final AbstractEvalResult result = CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE)); if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) { // Use EvalResult.TRUE instead of the real result so that solution variables are not displayed. return CommandUtils.displayDataForEvalResult(EvalResult.TRUE); diff --git a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java index 28cce18..557c4e7 100644 --- a/src/main/java/de/prob2/jupyter/commands/CommandUtils.java +++ b/src/main/java/de/prob2/jupyter/commands/CommandUtils.java @@ -8,6 +8,7 @@ import java.util.LinkedHashSet; import java.util.List; import java.util.Map; import java.util.Set; +import java.util.function.Supplier; import java.util.regex.Matcher; import java.util.regex.Pattern; import java.util.stream.Collectors; @@ -19,6 +20,7 @@ import de.prob.animator.domainobjects.ComputationNotCompletedResult; import de.prob.animator.domainobjects.EnumerationWarning; import de.prob.animator.domainobjects.EvalResult; import de.prob.animator.domainobjects.EvaluationErrorResult; +import de.prob.exception.ProBError; import de.prob.statespace.Trace; import de.prob.unicode.UnicodeTranslator; @@ -96,6 +98,21 @@ public final class CommandUtils { return preferences; } + public static <T> T withSourceCode(final @NotNull String code, final Supplier<T> action) { + try { + return action.get(); + } catch (final ProBError e) { + throw new WithSourceCodeException(code, e); + } + } + + public static void withSourceCode(final @NotNull String code, final Runnable action) { + withSourceCode(code, () -> { + action.run(); + return null; + }); + } + public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) { final StringBuilder sb = new StringBuilder(); final StringBuilder sbMarkdown = new StringBuilder(); diff --git a/src/main/java/de/prob2/jupyter/commands/DotCommand.java b/src/main/java/de/prob2/jupyter/commands/DotCommand.java index c57d9c7..ac43f77 100644 --- a/src/main/java/de/prob2/jupyter/commands/DotCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/DotCommand.java @@ -77,7 +77,9 @@ public final class DotCommand implements Command { final String command = split.get(0); final List<IEvalElement> args; if (split.size() > 1) { - args = Collections.singletonList(this.animationSelector.getCurrentTrace().getModel().parseFormula(split.get(1), FormulaExpand.EXPAND)); + final String code = split.get(1); + final IEvalElement formula = CommandUtils.withSourceCode(code, () -> this.animationSelector.getCurrentTrace().getModel().parseFormula(code, FormulaExpand.EXPAND)); + args = Collections.singletonList(formula); } else { args = Collections.emptyList(); } diff --git a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java index ab89659..8d2e75c 100644 --- a/src/main/java/de/prob2/jupyter/commands/EvalCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/EvalCommand.java @@ -38,7 +38,7 @@ public final class EvalCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { - return CommandUtils.displayDataForEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.EXPAND)); + return CommandUtils.displayDataForEvalResult(CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.EXPAND))); } @Override diff --git a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java index 1f563a6..9213744 100644 --- a/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/LoadCellCommand.java @@ -56,7 +56,9 @@ public final class LoadCellCommand implements Command { final List<String> args = CommandUtils.splitArgs(prefsString); final Map<String, String> preferences = CommandUtils.parsePreferences(args); - this.animationSelector.changeCurrentAnimation(new Trace(this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences))); + this.animationSelector.changeCurrentAnimation(new Trace(CommandUtils.withSourceCode(body, () -> + this.classicalBFactory.create("(machine from Jupyter cell)", body).load(preferences) + ))); return new DisplayData("Loaded machine: " + this.animationSelector.getCurrentTrace().getStateSpace().getMainComponent()); } diff --git a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java index 61e5065..33c2a2d 100644 --- a/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/PrettyPrintCommand.java @@ -46,7 +46,7 @@ public final class PrettyPrintCommand implements Command { cmdUnicode.setOptimize(false); final PrettyPrintFormulaCommand cmdLatex = new PrettyPrintFormulaCommand(formula, PrettyPrintFormulaCommand.Mode.LATEX); cmdLatex.setOptimize(false); - this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex); + CommandUtils.withSourceCode(argString, () -> this.animationSelector.getCurrentTrace().getStateSpace().execute(cmdUnicode, cmdLatex)); final DisplayData ret = new DisplayData(cmdUnicode.getPrettyPrint()); ret.putLatex('$' + cmdLatex.getPrettyPrint() + '$'); diff --git a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java index 77b2970..6b451e5 100644 --- a/src/main/java/de/prob2/jupyter/commands/SolveCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/SolveCommand.java @@ -67,7 +67,8 @@ public final class SolveCommand implements Command { if (solver == null) { throw new UserErrorException("Unknown solver: " + split.get(0)); } - final IEvalElement predicate = trace.getModel().parseFormula(split.get(1), FormulaExpand.EXPAND); + final String code = split.get(1); + final IEvalElement predicate = CommandUtils.withSourceCode(code, () -> trace.getModel().parseFormula(code, FormulaExpand.EXPAND)); final CbcSolveCommand cmd = new CbcSolveCommand(predicate, solver, this.animationSelector.getCurrentTrace().getCurrentState()); trace.getStateSpace().execute(cmd); diff --git a/src/main/java/de/prob2/jupyter/commands/TableCommand.java b/src/main/java/de/prob2/jupyter/commands/TableCommand.java index 9b9e131..494fe05 100644 --- a/src/main/java/de/prob2/jupyter/commands/TableCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/TableCommand.java @@ -49,7 +49,7 @@ public final class TableCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); - final IEvalElement formula = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND); + final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND)); final GetAllTableCommands cmd1 = new GetAllTableCommands(trace.getCurrentState()); trace.getStateSpace().execute(cmd1); diff --git a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java index 96a6b14..fcb3d26 100644 --- a/src/main/java/de/prob2/jupyter/commands/TypeCommand.java +++ b/src/main/java/de/prob2/jupyter/commands/TypeCommand.java @@ -42,7 +42,7 @@ public final class TypeCommand implements Command { @Override public @NotNull DisplayData run(final @NotNull String argString) { final Trace trace = this.animationSelector.getCurrentTrace(); - final IEvalElement formula = trace.getModel().parseFormula(argString, FormulaExpand.EXPAND); + final IEvalElement formula = CommandUtils.withSourceCode(argString, () -> trace.getModel().parseFormula(argString, FormulaExpand.EXPAND)); final TypeCheckResult result = trace.getStateSpace().typeCheck(formula); if (result.isOk()) { return new DisplayData(result.getType()); diff --git a/src/main/java/de/prob2/jupyter/commands/WithSourceCodeException.java b/src/main/java/de/prob2/jupyter/commands/WithSourceCodeException.java new file mode 100644 index 0000000..71e4618 --- /dev/null +++ b/src/main/java/de/prob2/jupyter/commands/WithSourceCodeException.java @@ -0,0 +1,26 @@ +package de.prob2.jupyter.commands; + +import de.prob.exception.ProBError; + +import org.jetbrains.annotations.NotNull; + +public final class WithSourceCodeException extends RuntimeException { + private static final long serialVersionUID = 1L; + + private final @NotNull String sourceCode; + + public WithSourceCodeException(final @NotNull String sourceCode, final @NotNull ProBError cause) { + super(cause.toString(), cause); + + this.sourceCode = sourceCode; + } + + public @NotNull String getSourceCode() { + return this.sourceCode; + } + + @Override + public synchronized @NotNull ProBError getCause() { + return (ProBError)super.getCause(); + } +} -- GitLab