From 349f096618eaa371c48c95d458c10743f177014a Mon Sep 17 00:00:00 2001
From: dgelessus <dgelessus@users.noreply.github.com>
Date: Tue, 23 Mar 2021 16:01:41 +0100
Subject: [PATCH] Don't keep :let variables across machine loads

---
 CHANGELOG.md                                  |  1 +
 notebooks/tests/let.ipynb                     | 47 +++++++++++++++++++
 .../java/de/prob2/jupyter/ProBKernel.java     |  1 +
 3 files changed, 49 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 48425b2..162ab2f 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -6,6 +6,7 @@
 * Added a `:language` command to allow changing the language used to parse user input. For example `:language event_b` can be used to switch to Event-B syntax when a non-Event-B machine is loaded (or no machine at all).
 * Improved the performance of loading machines by reusing the existing instance of ProB instead of starting a new one for each machine.
 * Improved error highlighting for machines loaded from files and not from the notebook.
+* Local variables (created using `:let`) are now discarded when a new machine is loaded. Previously local variables would be remembered even across machine loads, which could lead to confusing behavior and errors.
 * Significantly refactored the logic for parsing commands and their arguments.
 	* This is an internal change and should not affect any user-visible behavior. That is, all inputs that were accepted by previous versions should still be accepted - if any previously valid inputs are no longer accepted, this is a bug.
 	* As a side effect, the inspection and code completion features now work better in a few edge cases.
diff --git a/notebooks/tests/let.ipynb b/notebooks/tests/let.ipynb
index 630ec72..968949c 100644
--- a/notebooks/tests/let.ipynb
+++ b/notebooks/tests/let.ipynb
@@ -308,6 +308,53 @@
    "source": [
     "m"
    ]
+  },
+  {
+   "cell_type": "markdown",
+   "metadata": {},
+   "source": [
+    "Local variables are not persisted when a new machine is loaded."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 14,
+   "metadata": {},
+   "outputs": [
+    {
+     "data": {
+      "text/plain": [
+       "Loaded machine: Empty"
+      ]
+     },
+     "execution_count": 14,
+     "metadata": {},
+     "output_type": "execute_result"
+    }
+   ],
+   "source": [
+    "::load\n",
+    "MACHINE Empty\n",
+    "END"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": 15,
+   "metadata": {},
+   "outputs": [
+    {
+     "ename": "CommandExecutionException",
+     "evalue": ":eval: Computation not completed: Unknown identifier \"hello\"",
+     "output_type": "error",
+     "traceback": [
+      "\u001b[1m\u001b[31m:eval: Computation not completed: Unknown identifier \"hello\"\u001b[0m"
+     ]
+    }
+   ],
+   "source": [
+    "hello"
+   ]
   }
  ],
  "metadata": {
diff --git a/src/main/java/de/prob2/jupyter/ProBKernel.java b/src/main/java/de/prob2/jupyter/ProBKernel.java
index c8ba0ad..0751bc9 100644
--- a/src/main/java/de/prob2/jupyter/ProBKernel.java
+++ b/src/main/java/de/prob2/jupyter/ProBKernel.java
@@ -320,6 +320,7 @@ public final class ProBKernel extends BaseKernel {
 			oldTrace.getStateSpace().kill();
 		}
 		this.setCurrentMachineDirectory(Paths.get(""));
+		this.getVariables().clear();
 	}
 	
 	private @NotNull Trace loadDefaultMachine(final @NotNull StateSpace stateSpace) {
-- 
GitLab