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
|
||||
(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
|
||||
|
@ -654,7 +648,6 @@ 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)
|
||||
|
@ -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."
|
||||
(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
|
||||
|
@ -1267,44 +1252,5 @@ 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