diff --git a/CHANGELOG.md b/CHANGELOG.md
index b8922b241ac5053facf02d0793645b677537f894..f7ce3363c476d13fac3e399158e6a437903c381b 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -3,6 +3,7 @@
## [(next version)](https://gitlab.cs.uni-duesseldorf.de/api/v4/projects/848/jobs/artifacts/master/raw/build/libs/prob2-jupyter-kernel-1.3.1-SNAPSHOT-all.jar?job=test)
* Updated ProB 2 to version 4.0.0-SNAPSHOT.
+* Added position information to formula evaluation errors (e. g. type or well-definedness errors).
* Disabled LaTeX formatting inside `:check` tables as well, because of the layout issues mentioned below.
## [1.3.0](https://www3.hhu.de/stups/downloads/prob2-jupyter/prob2-jupyter-kernel-1.3.0-all.jar)
diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index 8d6f5147887ad8e2aba1137613f0fd4b57dca405..a6b39cfeaefd4f8f000de42e77f68ec453e1c4c2 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -223,10 +223,10 @@
"outputs": [
{
"ename": "CommandExecutionException",
- "evalue": ":assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'",
+ "evalue": ":assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: Computation not completed: Type mismatch: Expected INTEGER, but was POW(_A) in '{}'\u001b[0m"
+ "\u001b[1m\u001b[31m:assert: Error while evaluating assertion: (ERROR: Type mismatch: Expected INTEGER, but was POW(_A) in '{}')\u001b[0m"
]
}
],
diff --git a/notebooks/tests/eval.ipynb b/notebooks/tests/eval.ipynb
index 6cdfedfcfbace8d6a9aae79c195358447829339f..a3ca672857192e2bb8f566b06919f8eedcd6d47d 100644
--- a/notebooks/tests/eval.ipynb
+++ b/notebooks/tests/eval.ipynb
@@ -242,11 +242,13 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: Computation not completed: Unknown identifier \"unknown\"",
+ "ename": "ProBError",
+ "evalue": "ERROR\nProB returned error messages:\nError: Unknown identifier \"unknown\" (:1:0 to 1:7)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"unknown\"\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mERROR\u001b[0m",
+ "\u001b[1m\u001b[31mError: Unknown identifier \"unknown\" (:1:0 to 1:7)\u001b[0m",
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
@@ -260,11 +262,11 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: UNKNOWN (FALSE with enumeration warning)",
+ "ename": "ProBError",
+ "evalue": "UNKNOWN (enumeration warning)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: UNKNOWN (FALSE with enumeration warning)\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mUNKNOWN (enumeration warning)\u001b[0m"
]
}
],
@@ -278,13 +280,13 @@
"metadata": {},
"outputs": [
{
- "ename": "CommandExecutionException",
- "evalue": ":eval: NOT-WELL-DEFINED: \nmod not defined for negative numbers: 2 mod-1\n ### Line: 1, Column: 0 until 8\n\n",
+ "ename": "ProBError",
+ "evalue": "NOT-WELL-DEFINED\nProB returned error messages:\nError: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8)",
"output_type": "error",
"traceback": [
- "\u001b[1m\u001b[31m:eval: NOT-WELL-DEFINED: \u001b[0m",
- "\u001b[1m\u001b[31mmod not defined for negative numbers: 2 mod-1\u001b[0m",
- "\u001b[1m\u001b[31m ### Line: 1, Column: 0 until 8\u001b[0m"
+ "\u001b[1m\u001b[30mError from ProB: \u001b[0m\u001b[1m\u001b[31mNOT-WELL-DEFINED\u001b[0m",
+ "\u001b[1m\u001b[31mError: mod not defined for negative numbers: 2 mod-1 (:1:0 to 1:8)\u001b[0m",
+ "\u001b[1m\u001b[30m// Source code not known\u001b[0m"
]
}
],
diff --git a/src/main/java/de/prob2/jupyter/CommandUtils.java b/src/main/java/de/prob2/jupyter/CommandUtils.java
index 1951b387ff59295647c485a0058cc17ef2c16d14..692931f72662e80655e9cfebb81772ad6475dd09 100644
--- a/src/main/java/de/prob2/jupyter/CommandUtils.java
+++ b/src/main/java/de/prob2/jupyter/CommandUtils.java
@@ -18,16 +18,14 @@ import de.prob.animator.command.GetCurrentPreferencesCommand;
import de.prob.animator.command.GetDefaultPreferencesCommand;
import de.prob.animator.command.GetPreferenceCommand;
import de.prob.animator.domainobjects.AbstractEvalResult;
-import de.prob.animator.domainobjects.ComputationNotCompletedResult;
import de.prob.animator.domainobjects.EnumerationWarning;
+import de.prob.animator.domainobjects.ErrorItem;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.EvaluationErrorResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
-import de.prob.animator.domainobjects.IdentifierNotInitialised;
import de.prob.animator.domainobjects.ProBPreference;
import de.prob.animator.domainobjects.TypeCheckResult;
-import de.prob.animator.domainobjects.WDError;
import de.prob.exception.ProBError;
import de.prob.formula.PredicateBuilder;
import de.prob.statespace.Trace;
@@ -258,7 +256,6 @@ public final class CommandUtils {
public static @NotNull DisplayData displayDataForEvalResult(final @NotNull AbstractEvalResult aer) {
final StringBuilder sb = new StringBuilder();
final StringBuilder sbMarkdown = new StringBuilder();
- final boolean error;
if (aer instanceof EvalResult) {
final EvalResult result = (EvalResult)aer;
sb.append(UnicodeTranslator.toUnicode(result.getValue()));
@@ -280,75 +277,47 @@ public final class CommandUtils {
sbMarkdown.append('$');
});
}
- error = false;
- } else if (aer instanceof ComputationNotCompletedResult) {
- final ComputationNotCompletedResult result = (ComputationNotCompletedResult)aer;
- sb.append("Computation not completed: ");
- sb.append(result.getReason());
- error = true;
} else if (aer instanceof EnumerationWarning) {
- sb.append("UNKNOWN (FALSE with enumeration warning)");
- error = true;
+ throw new ProBError(aer.toString());
} else if (aer instanceof EvaluationErrorResult) {
final EvaluationErrorResult result = (EvaluationErrorResult)aer;
- sb.append(result.getResult());
- if (!result.getErrors().isEmpty()) {
- sb.append(": ");
- result.getErrors().forEach(s -> {
- sb.append('\n');
- sb.append(s);
- });
- }
- error = true;
+ throw new ProBError(result.getResult(), result.getErrorItems());
} else {
- LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
sb.append(aer);
sbMarkdown.append(aer);
- error = false;
}
- if (error) {
- throw new UserErrorException(sb.toString());
- } else {
- final DisplayData result = new DisplayData(sb.toString());
- result.putMarkdown(sbMarkdown.toString());
- return result;
- }
+ final DisplayData result = new DisplayData(sb.toString());
+ result.putMarkdown(sbMarkdown.toString());
+ return result;
}
public static @NotNull String inlinePlainTextForEvalResult(final @NotNull AbstractEvalResult aer) {
if (aer instanceof EvalResult) {
return UnicodeTranslator.toUnicode(((EvalResult)aer).getValue());
- } else if (aer instanceof ComputationNotCompletedResult) {
- return "(computation not completed: " + ((ComputationNotCompletedResult)aer).getReason() + ')';
- } else if (aer instanceof IdentifierNotInitialised) {
- return "(not initialised)";
- } else if (aer instanceof WDError) {
- return "(not well-defined)";
} else if (aer instanceof EvaluationErrorResult) {
- LOGGER.warn("Unknown evaluation error of type {}: {}", aer.getClass(), aer);
- return "(evaluation error: " + ((EvaluationErrorResult)aer).getErrors() + ')';
+ final EvaluationErrorResult result = (EvaluationErrorResult)aer;
+ final StringBuilder sb = new StringBuilder("(");
+ sb.append(result.getResult());
+ if (!result.getErrorItems().isEmpty()) {
+ sb.append(": ");
+ sb.append(result.getErrorItems().stream()
+ .map(ErrorItem::getMessage)
+ .collect(Collectors.joining(", ")));
+ }
+ sb.append(")");
+ return sb.toString();
} else {
- LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
return aer.toString();
}
}
public static @NotNull String inlineMarkdownForEvalResult(final @NotNull AbstractEvalResult aer) {
- if (aer instanceof EvalResult) {
- return UnicodeTranslator.toUnicode(((EvalResult)aer).getValue());
- } else if (aer instanceof ComputationNotCompletedResult) {
- return "*(computation not completed: " + ((ComputationNotCompletedResult)aer).getReason() + ")*";
- } else if (aer instanceof IdentifierNotInitialised) {
- return "*(not initialised)*";
- } else if (aer instanceof WDError) {
- return "*(not well-defined)*";
- } else if (aer instanceof EvaluationErrorResult) {
- LOGGER.warn("Unknown evaluation error of type {}: {}", aer.getClass(), aer);
- return "*(evaluation error: " + ((EvaluationErrorResult)aer).getErrors() + ")*";
+ if (aer instanceof EvaluationErrorResult) {
+ // Display errors in italics
+ return "*" + inlinePlainTextForEvalResult(aer) + "*";
} else {
- LOGGER.warn("Unknown eval result of type {}, falling back to toString(): {}", aer.getClass(), aer);
- return aer.toString();
+ return inlinePlainTextForEvalResult(aer);
}
}
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 31a2f55f818ba583a8e19b2d58d43469b06472c6..9c974c0afcc9de2edd0f66ebda38d2379e6592d2 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -9,6 +9,7 @@ import de.prob.animator.domainobjects.AbstractEvalResult;
import de.prob.animator.domainobjects.EvalResult;
import de.prob.animator.domainobjects.FormulaExpand;
import de.prob.animator.domainobjects.IEvalElement;
+import de.prob.exception.ProBError;
import de.prob.statespace.AnimationSelector;
import de.prob2.jupyter.Command;
import de.prob2.jupyter.CommandUtils;
@@ -81,8 +82,8 @@ public final class AssertCommand implements Command {
final DisplayData displayData;
try {
displayData = CommandUtils.displayDataForEvalResult(result);
- } catch (final UserErrorException e) {
- throw new UserErrorException("Error while evaluating assertion: " + e.getMessage());
+ } catch (final ProBError e) {
+ throw new UserErrorException("Error while evaluating assertion: " + CommandUtils.inlinePlainTextForEvalResult(result), e);
}
throw new UserErrorException("Assertion is not true: " + displayData.getData(MIMEType.TEXT_PLAIN));
}