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
|
||||
(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)
|
||||
|
Loading…
Reference in New Issue
Block a user