Add TLA+ Repl Shell elisp wrapper
- add a function to start a REPL TLA+ shell - add menu button to launch repl shell
This commit is contained in:
parent
71b6abbf9d
commit
09941c5311
|
@ -392,6 +392,12 @@
|
||||||
;; Main Menu
|
;; Main Menu
|
||||||
(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
|
(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]
|
(bindings--define-key map [menu-bar tla+ tla+-run-model]
|
||||||
'(menu-item "Run TLC Model Checker" tla+-run-model
|
'(menu-item "Run TLC Model Checker" tla+-run-model
|
||||||
:help
|
: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."
|
A \\cdot B describes the composition of actions A, B."
|
||||||
(interactive) (insert " A \\cdot 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)
|
(defun tla+-run-tlatex (type)
|
||||||
"Run TLaTeX and generate DVI, PDF or PS file.
|
"Run TLaTeX and generate DVI, PDF or PS file.
|
||||||
This function runs `pdflatex(1)' and geneartes a DVI file which can
|
This function runs `pdflatex(1)' and geneartes a DVI file which can
|
||||||
|
|
Loading…
Reference in New Issue