Compare commits
No commits in common. "master" and "v0.0.1" have entirely different histories.
@ -1,2 +0,0 @@
|
|||||||
# 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")
|
|
Binary file not shown.
Before Width: | Height: | Size: 157 KiB |
@ -392,12 +392,6 @@
|
|||||||
;; 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
|
||||||
@ -654,7 +648,6 @@ 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)
|
||||||
@ -771,14 +764,6 @@ 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
|
||||||
@ -1267,44 +1252,5 @@ 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