From 4773b99464a7f302d45079506cf50bd072b30dbf Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Wed, 20 Jun 2018 13:41:33 +0200
Subject: [PATCH] Show TRUE instead of nothing when an assertion succeeds

---
 notebooks/tests/assert.ipynb                  | 74 +++++++++++++++++--
 .../prob2/jupyter/commands/AssertCommand.java |  6 +-
 2 files changed, 69 insertions(+), 11 deletions(-)

diff --git a/notebooks/tests/assert.ipynb b/notebooks/tests/assert.ipynb
index 6b2bfab..8e79a0f 100644
--- a/notebooks/tests/assert.ipynb
+++ b/notebooks/tests/assert.ipynb
@@ -33,14 +33,28 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Asserting a true predicate doesn't show anything."
+    "Asserting a true predicate shows $\\mathit{TRUE}$."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": 2,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 2,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":assert 1 = 1"
    ]
@@ -49,7 +63,21 @@
    "cell_type": "code",
    "execution_count": 3,
    "metadata": {},
-   "outputs": [],
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 3,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
    "source": [
     ":assert TRUE"
    ]
@@ -58,13 +86,43 @@
    "cell_type": "markdown",
    "metadata": {},
    "source": [
-    "Asserting a false predicate shows an error."
+    "Asserting a predicate doesn't show any solutions."
    ]
   },
   {
    "cell_type": "code",
    "execution_count": 4,
    "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/markdown": [
+       "$\\mathit{TRUE}$"
+      ],
+      "text/plain": [
+       "TRUE"
+      ]
+     },
+     "execution_count": 4,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    ":assert x > 1"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Asserting a false predicate shows an error."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 5,
+   "metadata": {},
    "outputs": [
     {
      "ename": "CommandExecutionException",
@@ -81,7 +139,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 5,
+   "execution_count": 6,
    "metadata": {},
    "outputs": [
     {
@@ -106,7 +164,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 6,
+   "execution_count": 7,
    "metadata": {},
    "outputs": [
     {
@@ -124,7 +182,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 7,
+   "execution_count": 8,
    "metadata": {},
    "outputs": [
     {
@@ -149,7 +207,7 @@
   },
   {
    "cell_type": "code",
-   "execution_count": 8,
+   "execution_count": 9,
    "metadata": {},
    "outputs": [
     {
diff --git a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
index 9b6efd7..d78e3ab 100644
--- a/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
+++ b/src/main/java/de/prob2/jupyter/commands/AssertCommand.java
@@ -14,7 +14,6 @@ import io.github.spencerpark.jupyter.kernel.display.DisplayData;
 import io.github.spencerpark.jupyter.kernel.display.mime.MIMEType;
 
 import org.jetbrains.annotations.NotNull;
-import org.jetbrains.annotations.Nullable;
 
 public final class AssertCommand implements Command {
 	private final @NotNull AnimationSelector animationSelector;
@@ -37,10 +36,11 @@ public final class AssertCommand implements Command {
 	}
 	
 	@Override
-	public @Nullable DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
+	public @NotNull DisplayData run(final @NotNull ProBKernel kernel, final @NotNull String argString) {
 		final AbstractEvalResult result = this.animationSelector.getCurrentTrace().evalCurrent(argString, FormulaExpand.TRUNCATE);
 		if (result instanceof EvalResult && "TRUE".equals(((EvalResult)result).getValue())) {
-			return null;
+			// Use EvalResult.TRUE instead of the real result so that solution variables are not displayed.
+			return CommandUtils.displayDataForEvalResult(EvalResult.TRUE);
 		}
 		
 		final DisplayData displayData;
-- 
GitLab