Compare commits
6 Commits
Author | SHA1 | Date | |
---|---|---|---|
|
bf13ea44db | ||
|
09941c5311 | ||
|
71b6abbf9d | ||
78a196b94d | |||
2d679612c1 | |||
|
9dc03f8cbc |
2
README.md
Normal file
2
README.md
Normal file
|
@ -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")
|
BIN
examples/emacs-tlaplus.png
Normal file
BIN
examples/emacs-tlaplus.png
Normal file
Binary file not shown.
After Width: | Height: | Size: 157 KiB |
|
@ -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
|
||||||
|
@ -648,6 +654,7 @@ Note: The TLA+ specification file is a relative path.
|
||||||
(output (shell-command-to-string cmd))
|
(output (shell-command-to-string cmd))
|
||||||
(dot (tla+-run-dot)))
|
(dot (tla+-run-dot)))
|
||||||
(save-excursion
|
(save-excursion
|
||||||
|
(message (concat "Ran cmd: " cmd))
|
||||||
(if tlcbuffer
|
(if tlcbuffer
|
||||||
(progn
|
(progn
|
||||||
(switch-to-buffer tlcbuffer)
|
(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."
|
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
|
||||||
|
@ -1252,5 +1267,44 @@ The procedure works by:
|
||||||
(use-local-map widget-keymap)
|
(use-local-map widget-keymap)
|
||||||
(widget-setup)))
|
(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)
|
(provide 'tla+-mode)
|
||||||
|
|
Loading…
Reference in New Issue
Block a user