From 09941c5311f4a5ce5215472eb5e139835aac94f3 Mon Sep 17 00:00:00 2001
From: Christian Barthel <bch@online.de>
Date: Fri, 19 Feb 2021 21:35:15 +0100
Subject: [PATCH] Add TLA+ Repl Shell elisp wrapper

- add a function to start a REPL TLA+ shell
- add menu button to launch repl shell
---
 lisp/tla+-mode.el | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el
index 9a5df23..d991981 100644
--- a/lisp/tla+-mode.el
+++ b/lisp/tla+-mode.el
@@ -392,6 +392,12 @@
     ;; Main Menu
     (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
 
+    (bindings--define-key map [menu-bar tla+ tla+-run-shell]
+      '(menu-item "Run TLA+ REPL Shell" tla+-run-shell
+                  :help
+                  "Run tlc2.REPL"
+                  "(Execute TLA+ Read Eval Print Loop)"))
+
     (bindings--define-key map [menu-bar tla+ tla+-run-model]
       '(menu-item "Run TLC Model Checker" tla+-run-model
                   :help
@@ -765,6 +771,14 @@ step is taken to a new state, i.e. e' = e. "
 A \\cdot B describes the composition of actions A, B."
   (interactive) (insert " A \\cdot B"))
 
+(defun tla+-run-shell ()
+  "Execute TLA REPL"
+  (interactive)
+  (shell (get-buffer-create "*TLA+ Repl*"))
+  ;; java -cp ../tla2tools.jar tlc2.REPL
+  (insert (format "%s -cp %s tlc2.REPL"
+		  tla+-java-path tla+-tlatools-path)))
+
 (defun tla+-run-tlatex (type)
   "Run TLaTeX and generate DVI, PDF or PS file.
 This function runs `pdflatex(1)' and geneartes a DVI file which can