Add a few tla symbols and load them to prettify them on command

- define some TLA+ symbols
- Use `M-x prettify-symbols-mode' to view them.

README.md

@@ -0,0 +1,2 @@
+# TLA+ Major Mode for GNU/Emacs
+![Emacs/TLA+ Mode](https://git.sdf.org/bch/tlamode/raw/branch/master/examples/emacs-tlaplus.png "Emacs TLA+ Mode")

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
@@ -648,6 +654,7 @@ Note: The TLA+ specification file is a relative path.
          (output (shell-command-to-string cmd))
          (dot    (tla+-run-dot)))
     (save-excursion
+      (message (concat "Ran cmd: " cmd))
       (if tlcbuffer
           (progn
             (switch-to-buffer tlcbuffer)
@@ -764,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
@@ -1252,5 +1267,44 @@ The procedure works by:
   (use-local-map widget-keymap)
   (widget-setup)))
 
+
+(defun tla+/load-symbols ()
+  "make some word or string show as pretty Unicode symbols"
+  (setq prettify-symbols-alist
+        '(
+	  ("<"   . ?<)
+	  (">"   . ?>)
+	  ("<>"  . ?◇)
+	  ("<="  . ?≤)
+	  ("\\leq"  . ?≤)
+	  ("\\geq"  . ?≥)
+	  (">="  . ?≥)
+	  ("~>" . ?⇝)
+	  ("\\E" . ?∃)
+	  ("\\A" . ?∀)
+	  ("\\cup" . ?∪)
+	  ("\\union" . ?∪)
+	  ("\\cap" . ?∩)
+	  ("\\intersect" . ?∩)
+	  ("\\in"    . ?∈)
+	  ("\\notin" . ?∉)
+	  ("#" . ?≠)
+	  ("/=" . ?≠)
+	  ("<<" . ?⟨ )
+	   (">>" . ?⟩ )
+	  ("[]" . ?□)
+	  ("\\equiv" . ?≡)
+	  ("<=>"    . ?≡)
+	  ("/\\"    . ?∧)
+	  ("\\/"     . ?∨)
+          ("=>"     . ?⇒)    ; ⇒
+	  ("=="     . ?≜)
+	  ("\\neg"   . ?¬)
+	  ("\\lnot"  . ?¬)
+	  ("\\neg"   . ?¬)
+          )))
+
+(add-hook 'tla+-mode-hook 'tla+/load-symbols)
+
 
 (provide 'tla+-mode)