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

@@ -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": {

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 {
+					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;

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);

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();

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();
 		}

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

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());
 	}
 	

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() + '$');

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);

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);

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());

src/main/java/de/prob2/jupyter/commands/WithSourceCodeException.java

+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();
+	}
+}