Begin supporting use of native let variables on the Prolog side

src/main/java/de/prob2/jupyter/ProBKernel.java

@@ -40,6 +40,8 @@ import de.prob.animator.domainobjects.AbstractEvalResult;
 import de.prob.animator.domainobjects.ClassicalB;
 import de.prob.animator.domainobjects.ErrorItem;
 import de.prob.animator.domainobjects.EvalElementType;
+import de.prob.animator.domainobjects.EvalExpandMode;
+import de.prob.animator.domainobjects.EvalOptions;
 import de.prob.animator.domainobjects.EvalResult;
 import de.prob.animator.domainobjects.EventB;
 import de.prob.animator.domainobjects.FormulaExpand;
@@ -149,6 +151,13 @@ public final class ProBKernel extends BaseKernel {
 	private static final @NotNull Pattern BSYMB_COMMAND_PATTERN = Pattern.compile("\\\\([a-z]+)");
 	private static final @NotNull Pattern LATEX_FORMULA_PATTERN = Pattern.compile("(\\$\\$?)([^\\$]+)\\1");
 	
+	public static final @NotNull EvalOptions EVAL_OPTIONS = EvalOptions.DEFAULT
+		.withProvideStoredLetValues(true)
+		.withEvalExpand(EvalExpandMode.EFFICIENT);
+	public static final @NotNull EvalOptions TRUNCATE_EVAL_OPTIONS = EVAL_OPTIONS
+		.withEvalExpand(EvalExpandMode.NEVER)
+		.withExpand(FormulaExpand.TRUNCATE);
+	
 	private static final @NotNull Collection<@NotNull Class<? extends Command>> COMMAND_CLASSES = Collections.unmodifiableList(Arrays.asList(
 		AssertCommand.class,
 		BrowseCommand.class,

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

@@ -72,7 +72,7 @@ public final class AssertCommand implements Command {
 		final ProBKernel kernel = this.kernelProvider.get();
 		final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.TRUNCATE);
 		final AbstractEvalResult result = CommandUtils.withSourceCode(formula, () -> 
-			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.TRUNCATE_EVAL_OPTIONS))
 		);
 		if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
 			// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.

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

@@ -67,7 +67,7 @@ public final class EvalCommand implements Command {
 		final ProBKernel kernel = this.injector.getInstance(ProBKernel.class);
 		final IEvalElement formula = kernel.parseFormula(args.get(FORMULA_PARAM), FormulaExpand.EXPAND);
 		return CommandUtils.withSourceCode(formula, () -> {
-			final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula);
+			final AbstractEvalResult aer = this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS);
 			return CommandUtils.displayDataForEvalResult(kernel.postprocessEvalResult(aer));
 		});
 	}

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

@@ -80,7 +80,7 @@ public final class LetCommand implements Command {
 		final ProBKernel kernel = this.kernelProvider.get();
 		final IEvalElement formula = kernel.parseFormula(expression, FormulaExpand.EXPAND);
 		final AbstractEvalResult evaluated = CommandUtils.withSourceCode(formula, () ->
-			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula))
+			kernel.postprocessEvalResult(this.animationSelector.getCurrentTrace().evalCurrent(formula, ProBKernel.EVAL_OPTIONS))
 		);
 		if (evaluated instanceof EvalResult) {
 			kernel.getVariables().put(name, ((EvalResult)evaluated).getValue());