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 |
|
@ -129,22 +129,22 @@
|
||||||
(menu-map (make-sparse-keymap "TLA+"))
|
(menu-map (make-sparse-keymap "TLA+"))
|
||||||
|
|
||||||
(operator-map (make-sparse-keymap))
|
(operator-map (make-sparse-keymap))
|
||||||
|
|
||||||
(action-operator-map (make-sparse-keymap))
|
(action-operator-map (make-sparse-keymap))
|
||||||
(temporal-operator-map (make-sparse-keymap))
|
(temporal-operator-map (make-sparse-keymap))
|
||||||
(export-map (make-sparse-keymap))
|
(export-map (make-sparse-keymap))
|
||||||
|
|
||||||
(modul-operators (make-sparse-keymap))
|
(modul-operators (make-sparse-keymap))
|
||||||
(modul-sequences-operators (make-sparse-keymap))
|
(modul-sequences-operators (make-sparse-keymap))
|
||||||
(modul-naturals-operators (make-sparse-keymap))
|
(modul-naturals-operators (make-sparse-keymap))
|
||||||
)
|
)
|
||||||
(set-keymap-parent map lisp-mode-shared-map)
|
(set-keymap-parent map lisp-mode-shared-map)
|
||||||
(define-key map "\e\t" 'ispell-complete-word)
|
(define-key map "\e\t" 'ispell-complete-word)
|
||||||
(define-key map (kbd "C-c C-t e") 'tla+-run-tlatex-dvi)
|
(define-key map (kbd "C-c C-t e") 'tla+-run-tlatex-dvi)
|
||||||
(define-key map (kbd "C-c C-t o") 'tla+-open-dvi)
|
(define-key map (kbd "C-c C-t o") 'tla+-open-dvi)
|
||||||
(define-key map (kbd "C-c C-t c") 'tla+-run-sany)
|
(define-key map (kbd "C-c C-t c") 'tla+-run-sany)
|
||||||
(define-key map (kbd "C-c C-t p") 'tla+-run-pluscal)
|
(define-key map (kbd "C-c C-t p") 'tla+-run-pluscal)
|
||||||
(define-key map (kbd "C-c C-t m") 'tla+-run-model)
|
(define-key map (kbd "C-c C-t m") 'tla+-run-model)
|
||||||
|
|
||||||
;; Main TLA+ Menu:
|
;; Main TLA+ Menu:
|
||||||
(bindings--define-key map [menu-bar tla+]
|
(bindings--define-key map [menu-bar tla+]
|
||||||
|
@ -152,7 +152,7 @@
|
||||||
|
|
||||||
;; Modul Operators
|
;; Modul Operators
|
||||||
(bindings--define-key menu-map [modul-operators]
|
(bindings--define-key menu-map [modul-operators]
|
||||||
(cons "Insert Modul Operator.." modul-operators))
|
(cons "Insert Modul Operator.." modul-operators))
|
||||||
|
|
||||||
;; Naturals Operators
|
;; Naturals Operators
|
||||||
(bindings--define-key modul-operators
|
(bindings--define-key modul-operators
|
||||||
|
@ -172,7 +172,7 @@
|
||||||
(lambda () (interactive)
|
(lambda () (interactive)
|
||||||
(insert "-")
|
(insert "-")
|
||||||
(backward-char 2))
|
(backward-char 2))
|
||||||
:help "Subtraction"))
|
:help "Subtraction"))
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
modul-naturals-operators [mult-nat]
|
modul-naturals-operators [mult-nat]
|
||||||
|
@ -186,7 +186,7 @@
|
||||||
'(menu-item "/"
|
'(menu-item "/"
|
||||||
(lambda () (interactive)
|
(lambda () (interactive)
|
||||||
(insert "/"))
|
(insert "/"))
|
||||||
:help "Division"))
|
:help "Division"))
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
modul-naturals-operators [exp-nat]
|
modul-naturals-operators [exp-nat]
|
||||||
|
@ -217,7 +217,7 @@
|
||||||
(insert "%"))
|
(insert "%"))
|
||||||
:help "Modulo"))
|
:help "Modulo"))
|
||||||
|
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
modul-naturals-operators [leq-nat]
|
modul-naturals-operators [leq-nat]
|
||||||
'(menu-item "\\leq"
|
'(menu-item "\\leq"
|
||||||
|
@ -231,7 +231,7 @@
|
||||||
(lambda () (interactive)
|
(lambda () (interactive)
|
||||||
(insert "\\geq"))
|
(insert "\\geq"))
|
||||||
:help "Greater Equal"))
|
:help "Greater Equal"))
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
modul-naturals-operators [lt-nat]
|
modul-naturals-operators [lt-nat]
|
||||||
'(menu-item "<"
|
'(menu-item "<"
|
||||||
|
@ -246,7 +246,7 @@
|
||||||
(insert ">"))
|
(insert ">"))
|
||||||
:help "Greater than"))
|
:help "Greater than"))
|
||||||
|
|
||||||
|
|
||||||
;; Sequence Operators
|
;; Sequence Operators
|
||||||
(bindings--define-key modul-operators
|
(bindings--define-key modul-operators
|
||||||
[modul-sequences-operator]
|
[modul-sequences-operator]
|
||||||
|
@ -260,7 +260,7 @@
|
||||||
(backward-char 2))
|
(backward-char 2))
|
||||||
:help
|
:help
|
||||||
"Set of all Sequences of Elements of Set `S'"))
|
"Set of all Sequences of Elements of Set `S'"))
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
modul-sequences-operators [head-s]
|
modul-sequences-operators [head-s]
|
||||||
'(menu-item "Head(s)"
|
'(menu-item "Head(s)"
|
||||||
|
@ -301,7 +301,7 @@
|
||||||
(backward-char 2))
|
(backward-char 2))
|
||||||
:help "length of sequence s"))
|
:help "length of sequence s"))
|
||||||
|
|
||||||
|
|
||||||
;; Operators
|
;; Operators
|
||||||
(bindings--define-key menu-map [operator]
|
(bindings--define-key menu-map [operator]
|
||||||
(cons "Insert Operator.." operator-map))
|
(cons "Insert Operator.." operator-map))
|
||||||
|
@ -314,7 +314,7 @@
|
||||||
action-operator-map [primed-operator]
|
action-operator-map [primed-operator]
|
||||||
'(menu-item "e'" tla+-operator-primed
|
'(menu-item "e'" tla+-operator-primed
|
||||||
:help "Value of e in final state of a step"))
|
:help "Value of e in final state of a step"))
|
||||||
|
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
action-operator-map [stutter-operator]
|
action-operator-map [stutter-operator]
|
||||||
'(menu-item "[A]_e" tla+-operator-stutter
|
'(menu-item "[A]_e" tla+-operator-stutter
|
||||||
|
@ -338,8 +338,8 @@
|
||||||
(bindings--define-key
|
(bindings--define-key
|
||||||
action-operator-map [composition-operator]
|
action-operator-map [composition-operator]
|
||||||
'(menu-item "A \\cdot B" tla+-operator-composition
|
'(menu-item "A \\cdot B" tla+-operator-composition
|
||||||
:help "Composition of actions"))
|
:help "Composition of actions"))
|
||||||
|
|
||||||
;; Temporal operators:
|
;; Temporal operators:
|
||||||
(bindings--define-key operator-map [temporal-operator]
|
(bindings--define-key operator-map [temporal-operator]
|
||||||
(cons "Temporal Operator" temporal-operator-map))
|
(cons "Temporal Operator" temporal-operator-map))
|
||||||
|
@ -368,11 +368,11 @@
|
||||||
temporal-operator-map [leadsto-temporal-operator]
|
temporal-operator-map [leadsto-temporal-operator]
|
||||||
'(menu-item "F ~> G" tla+-operator-leadsto
|
'(menu-item "F ~> G" tla+-operator-leadsto
|
||||||
:help "F leads to G"))
|
:help "F leads to G"))
|
||||||
|
|
||||||
;; Export Menu:
|
;; Export Menu:
|
||||||
(bindings--define-key menu-map [export]
|
(bindings--define-key menu-map [export]
|
||||||
(cons "Export.." export-map))
|
(cons "Export.." export-map))
|
||||||
|
|
||||||
(bindings--define-key export-map [export-pdf]
|
(bindings--define-key export-map [export-pdf]
|
||||||
'(menu-item "Run TLatex and create PDF" tla+-run-tlatex-pdf
|
'(menu-item "Run TLatex and create PDF" tla+-run-tlatex-pdf
|
||||||
:help "Typeset TLaTex and create PDF Document"))
|
:help "Typeset TLaTex and create PDF Document"))
|
||||||
|
@ -384,7 +384,7 @@
|
||||||
(bindings--define-key export-map [export-ps]
|
(bindings--define-key export-map [export-ps]
|
||||||
'(menu-item "Run TLatex and create PS" tla+-run-tlatex-ps
|
'(menu-item "Run TLatex and create PS" tla+-run-tlatex-ps
|
||||||
:help "Typeset TLaTex and create PS Document"))
|
:help "Typeset TLaTex and create PS Document"))
|
||||||
|
|
||||||
(bindings--define-key export-map [export-open]
|
(bindings--define-key export-map [export-open]
|
||||||
'(menu-item "Open DVI Viewer" tla+-open-dvi
|
'(menu-item "Open DVI Viewer" tla+-open-dvi
|
||||||
:help "Open DVI Viewer"))
|
:help "Open DVI Viewer"))
|
||||||
|
@ -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
|
||||||
|
@ -404,13 +410,13 @@
|
||||||
"Create a TLC Model"
|
"Create a TLC Model"
|
||||||
"(Open the TLC Configuration dialogue)"))
|
"(Open the TLC Configuration dialogue)"))
|
||||||
|
|
||||||
|
|
||||||
(bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
|
(bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
|
||||||
'(menu-item "Run PlusCal Translator" tla+-run-pluscal
|
'(menu-item "Run PlusCal Translator" tla+-run-pluscal
|
||||||
:help
|
:help
|
||||||
"Run pcal.trans"
|
"Run pcal.trans"
|
||||||
"(Translator (PlusCal algorithm language -> TLA+)"))
|
"(Translator (PlusCal algorithm language -> TLA+)"))
|
||||||
|
|
||||||
(bindings--define-key map [menu-bar tla+ tla+-run-sany]
|
(bindings--define-key map [menu-bar tla+ tla+-run-sany]
|
||||||
'(menu-item "Run Syntax Checker" tla+-run-sany
|
'(menu-item "Run Syntax Checker" tla+-run-sany
|
||||||
:help
|
:help
|
||||||
|
@ -420,7 +426,7 @@
|
||||||
(bindings--define-key map [menu-bar tla+ tla+-update-note]
|
(bindings--define-key map [menu-bar tla+ tla+-update-note]
|
||||||
'(menu-item "Add Update Comment" tla+-add-update-note
|
'(menu-item "Add Update Comment" tla+-add-update-note
|
||||||
:help "Add Update Note"))
|
:help "Add Update Note"))
|
||||||
|
|
||||||
(bindings--define-key map [menu-bar tla+ tla+-create-module]
|
(bindings--define-key map [menu-bar tla+ tla+-create-module]
|
||||||
'(menu-item "Create new Module" tla+-create-module
|
'(menu-item "Create new Module" tla+-create-module
|
||||||
:help "Create a new TLA+ Module"))
|
:help "Create a new TLA+ Module"))
|
||||||
|
@ -432,10 +438,10 @@
|
||||||
(defconst tla+-font-lock-keywords
|
(defconst tla+-font-lock-keywords
|
||||||
(list
|
(list
|
||||||
'("\\\\\\*.*$" . font-lock-comment-face)
|
'("\\\\\\*.*$" . font-lock-comment-face)
|
||||||
'("(\\*.*\\*)" . font-lock-comment-face)
|
'("(\\*.*\\*)" . font-lock-comment-face)
|
||||||
'("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|LOCAL\\|ASSUME\\|LET\\|EXTENDS?\\)\\>"
|
'("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|LOCAL\\|ASSUME\\|LET\\|EXTENDS?\\)\\>"
|
||||||
. font-lock-builtin-face)
|
. font-lock-builtin-face)
|
||||||
'("\\<\\(TRUE\\|FALSE\\|OTHER\\|BOOLEAN\\|DOMAIN\\)\\>" . font-lock-type-face)
|
'("\\<\\(TRUE\\|FALSE\\|OTHER\\|BOOLEAN\\|DOMAIN\\)\\>" . font-lock-type-face)
|
||||||
'("\\<\\(CONSTANT\\|SUBSET\\|ENABLED\\|UNCHANGED\\|INSTANCE\\|WITH\\|EXCEPT\\|UNION\\|IN\\|DOMAIN\\|EXCEPT\\|IF\\|THEN\\|ELSE\\|CHOOSE\\)\\>" . font-lock-keyword-face)
|
'("\\<\\(CONSTANT\\|SUBSET\\|ENABLED\\|UNCHANGED\\|INSTANCE\\|WITH\\|EXCEPT\\|UNION\\|IN\\|DOMAIN\\|EXCEPT\\|IF\\|THEN\\|ELSE\\|CHOOSE\\)\\>" . font-lock-keyword-face)
|
||||||
|
|
||||||
'("\\('\\w*'\\)" . font-lock-variable-name-face)
|
'("\\('\\w*'\\)" . font-lock-variable-name-face)
|
||||||
|
@ -445,14 +451,14 @@
|
||||||
;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode))
|
;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode))
|
||||||
;;;###autoload
|
;;;###autoload
|
||||||
(define-derived-mode tla+-mode fundamental-mode "TLA+"
|
(define-derived-mode tla+-mode fundamental-mode "TLA+"
|
||||||
"Major mode for editing TLA+ specification files.
|
"Major mode for editing TLA+ specification files.
|
||||||
|
|
||||||
This package defines TLA+ Major Mode to manipulate TLA+
|
This package defines TLA+ Major Mode to manipulate TLA+
|
||||||
specifications as invented by Leslie Lamport [1].
|
specifications as invented by Leslie Lamport [1].
|
||||||
|
|
||||||
In this mode, syntax highlighting is activated for TLA+
|
In this mode, syntax highlighting is activated for TLA+
|
||||||
specification files. Various operators can be inserted
|
specification files. Various operators can be inserted
|
||||||
by `tla+-operator-NAME'.
|
by `tla+-operator-NAME'.
|
||||||
|
|
||||||
Features:
|
Features:
|
||||||
- Syntax Highlighting for TLA+ Specification Files
|
- Syntax Highlighting for TLA+ Specification Files
|
||||||
|
@ -465,7 +471,7 @@ Features:
|
||||||
or typical Emacs keystrokes.
|
or typical Emacs keystrokes.
|
||||||
- Use templates to generate Modules
|
- Use templates to generate Modules
|
||||||
- An Emacs widget to create TLC configuration files
|
- An Emacs widget to create TLC configuration files
|
||||||
- Options to run the TLC model checker on TLA+
|
- Options to run the TLC model checker on TLA+
|
||||||
specifications (`C-c C-t m').
|
specifications (`C-c C-t m').
|
||||||
- Translate PlusCal code to TLA+ specification
|
- Translate PlusCal code to TLA+ specification
|
||||||
with `C-c C-t p'.
|
with `C-c C-t p'.
|
||||||
|
@ -485,7 +491,7 @@ Configuration:
|
||||||
(setq tla+-tlatools-path </path/to/tla2tools.jar>)
|
(setq tla+-tlatools-path </path/to/tla2tools.jar>)
|
||||||
or with:
|
or with:
|
||||||
M-x customize-group <RET> tla+
|
M-x customize-group <RET> tla+
|
||||||
|
|
||||||
You may also set the following paths:
|
You may also set the following paths:
|
||||||
tla+-java-path
|
tla+-java-path
|
||||||
tla+-dvipdf-path
|
tla+-dvipdf-path
|
||||||
|
@ -545,12 +551,12 @@ specification file."
|
||||||
(insert (concat "\\* " text))
|
(insert (concat "\\* " text))
|
||||||
(goto-char (- (point-max) (length text)))))
|
(goto-char (- (point-max) (length text)))))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(defun tla+-run-sany ()
|
(defun tla+-run-sany ()
|
||||||
"This function runs tla2sany.SANY (TLA syntax checker)
|
"This function runs tla2sany.SANY (TLA syntax checker)
|
||||||
The function executes the TLA+ Syntax checker and reports errors
|
The function executes the TLA+ Syntax checker and reports errors
|
||||||
in a new frame. Errors are clickable buttons and the user can
|
in a new frame. Errors are clickable buttons and the user can
|
||||||
directly go to the error line.
|
directly go to the error line.
|
||||||
|
|
||||||
It is meant to be run from a TLA+ Specification buffer.
|
It is meant to be run from a TLA+ Specification buffer.
|
||||||
|
@ -594,9 +600,9 @@ Operation:
|
||||||
"Run the tlc2.TLC Model checker
|
"Run the tlc2.TLC Model checker
|
||||||
Run the tlc2.TLC model checker on a TLA+ buffer with a given
|
Run the tlc2.TLC model checker on a TLA+ buffer with a given
|
||||||
moden CFGFILE. The function constructs an absolute path to
|
moden CFGFILE. The function constructs an absolute path to
|
||||||
a model file spec.cfg and uses the current buffer as TLA+
|
a model file spec.cfg and uses the current buffer as TLA+
|
||||||
specification. It then executes the tlc2.TLC model checker
|
specification. It then executes the tlc2.TLC model checker
|
||||||
with the given model.
|
with the given model.
|
||||||
|
|
||||||
Note: The TLA+ specification file is a relative path.
|
Note: The TLA+ specification file is a relative path.
|
||||||
"
|
"
|
||||||
|
@ -609,7 +615,7 @@ Note: The TLA+ specification file is a relative path.
|
||||||
(file-name-base (buffer-file-name))
|
(file-name-base (buffer-file-name))
|
||||||
".cfg" ))))
|
".cfg" ))))
|
||||||
(if (not tla+-tlatools-path)
|
(if (not tla+-tlatools-path)
|
||||||
(error "need the TLA+ toolbox java archive: tla+-tlatools-path"))
|
(error "need the TLA+ toolbox java archive: tla+-tlatools-path"))
|
||||||
(let* ((filename (buffer-file-name))
|
(let* ((filename (buffer-file-name))
|
||||||
(tlcbufname (format "*tlc2.TLC* [%s]" (buffer-name)))
|
(tlcbufname (format "*tlc2.TLC* [%s]" (buffer-name)))
|
||||||
;(tlcbuffer (get-buffer-create
|
;(tlcbuffer (get-buffer-create
|
||||||
|
@ -642,12 +648,13 @@ Note: The TLA+ specification file is a relative path.
|
||||||
opt-simulate " "
|
opt-simulate " "
|
||||||
opt-depth " "
|
opt-depth " "
|
||||||
tla+-tlc-coverage " "
|
tla+-tlc-coverage " "
|
||||||
opt-workers " "
|
opt-workers " "
|
||||||
" -config " cfgfile " "
|
" -config " cfgfile " "
|
||||||
finame))
|
finame))
|
||||||
(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)
|
||||||
|
@ -667,14 +674,14 @@ Note: The TLA+ specification file is a relative path.
|
||||||
(setq buffer-read-only 't)
|
(setq buffer-read-only 't)
|
||||||
(other-window 1)))))))
|
(other-window 1)))))))
|
||||||
|
|
||||||
|
|
||||||
(defun tla+-run-pluscal ()
|
(defun tla+-run-pluscal ()
|
||||||
"This function runs pcal.trans (PlusCal Translator to TLA+)
|
"This function runs pcal.trans (PlusCal Translator to TLA+)
|
||||||
This function executes the PlusCal Translator on the current
|
This function executes the PlusCal Translator on the current
|
||||||
buffer (Assumption: the buffer is a TLA+ buffer that contains
|
buffer (Assumption: the buffer is a TLA+ buffer that contains
|
||||||
PlusCal code).
|
PlusCal code).
|
||||||
On success, the buffer will be reloaded and a message will be
|
On success, the buffer will be reloaded and a message will be
|
||||||
printed. On failure (i.e. the exit code of the shell command
|
printed. On failure (i.e. the exit code of the shell command
|
||||||
was not 0), an error message will be printed.
|
was not 0), an error message will be printed.
|
||||||
"
|
"
|
||||||
(interactive)
|
(interactive)
|
||||||
|
@ -683,7 +690,7 @@ was not 0), an error message will be printed.
|
||||||
".tla$" ".old" filename))
|
".tla$" ".old" filename))
|
||||||
(pcalbuf (get-buffer-create
|
(pcalbuf (get-buffer-create
|
||||||
(format "*pcal.trans* [%s]" (buffer-name))))
|
(format "*pcal.trans* [%s]" (buffer-name))))
|
||||||
(cmd (concat
|
(cmd (concat
|
||||||
tla+-java-path " -cp " tla+-tlatools-path
|
tla+-java-path " -cp " tla+-tlatools-path
|
||||||
" pcal.trans "filename ))
|
" pcal.trans "filename ))
|
||||||
(output (shell-command cmd)))
|
(output (shell-command cmd)))
|
||||||
|
@ -705,8 +712,8 @@ was not 0), an error message will be printed.
|
||||||
(insert
|
(insert
|
||||||
(shell-command-to-string cmd))
|
(shell-command-to-string cmd))
|
||||||
(message "Translation Failed")))))
|
(message "Translation Failed")))))
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(defun tla+-open-dvi (buffername)
|
(defun tla+-open-dvi (buffername)
|
||||||
"Function to open a DVI file.
|
"Function to open a DVI file.
|
||||||
|
@ -756,7 +763,7 @@ as DVI file.
|
||||||
(defun tla+-operator-unchanged ()
|
(defun tla+-operator-unchanged ()
|
||||||
"insert UNCHANGED operator.
|
"insert UNCHANGED operator.
|
||||||
Variables declared as unchanged will have the same value when a
|
Variables declared as unchanged will have the same value when a
|
||||||
step is taken to a new state, i.e. e' = e. "
|
step is taken to a new state, i.e. e' = e. "
|
||||||
(interactive) (insert " UNCHANGED e"))
|
(interactive) (insert " UNCHANGED e"))
|
||||||
|
|
||||||
(defun tla+-operator-cdot ()
|
(defun tla+-operator-cdot ()
|
||||||
|
@ -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
|
||||||
|
@ -804,18 +819,18 @@ The function executes one or two shell commands synchronously."
|
||||||
|
|
||||||
(defun tla+-run-tlatex-pdf ()
|
(defun tla+-run-tlatex-pdf ()
|
||||||
"Create PDF file from TLA+ Specification.
|
"Create PDF file from TLA+ Specification.
|
||||||
This function creates a PDF file of a TLA+ Specification by
|
This function creates a PDF file of a TLA+ Specification by
|
||||||
`tla+-run-tlatex'"
|
`tla+-run-tlatex'"
|
||||||
(interactive) (tla+-run-tlatex 'pdf))
|
(interactive) (tla+-run-tlatex 'pdf))
|
||||||
(defun tla+-run-tlatex-dvi ()
|
(defun tla+-run-tlatex-dvi ()
|
||||||
"Create DVI file from TLA+ Specification.
|
"Create DVI file from TLA+ Specification.
|
||||||
This function creates a DVI file of a TLA+ Specification by
|
This function creates a DVI file of a TLA+ Specification by
|
||||||
`tla+-run-tlatex'"
|
`tla+-run-tlatex'"
|
||||||
(interactive) (tla+-run-tlatex 'dvi))
|
(interactive) (tla+-run-tlatex 'dvi))
|
||||||
(defun tla+-run-tlatex-ps ()
|
(defun tla+-run-tlatex-ps ()
|
||||||
"Create PS file from TLA+ Specification.
|
"Create PS file from TLA+ Specification.
|
||||||
This function creates a PS file of a TLA+ Specification by
|
This function creates a PS file of a TLA+ Specification by
|
||||||
`tla+-run-tlatex'"
|
`tla+-run-tlatex'"
|
||||||
(interactive) (tla+-run-tlatex 'ps))
|
(interactive) (tla+-run-tlatex 'ps))
|
||||||
|
|
||||||
|
|
||||||
|
@ -833,8 +848,8 @@ This function creates a PS file of a TLA+ Specification by
|
||||||
|
|
||||||
(defun tla+/sany-button-pressed (button)
|
(defun tla+/sany-button-pressed (button)
|
||||||
"Find the position and goto a sany error position.
|
"Find the position and goto a sany error position.
|
||||||
This function will be executed when a user clicks on a button inside
|
This function will be executed when a user clicks on a button inside
|
||||||
the SANY error report buffer. This is done by selecting the other
|
the SANY error report buffer. This is done by selecting the other
|
||||||
window and going to the line mentioned in the error message.
|
window and going to the line mentioned in the error message.
|
||||||
The parameter BUTTON is currently unused.
|
The parameter BUTTON is currently unused.
|
||||||
|
|
||||||
|
@ -843,7 +858,7 @@ Steps done by this function:
|
||||||
2. get the text label of the button which is usually a line like
|
2. get the text label of the button which is usually a line like
|
||||||
line XX, column YY
|
line XX, column YY
|
||||||
3. Get line number and column count of the error message
|
3. Get line number and column count of the error message
|
||||||
4. select the other-window (it is assumed that this is the *.tla
|
4. select the other-window (it is assumed that this is the *.tla
|
||||||
specification where SANY was executed.
|
specification where SANY was executed.
|
||||||
5. goto line and column.
|
5. goto line and column.
|
||||||
"
|
"
|
||||||
|
@ -873,16 +888,16 @@ Steps done by this function:
|
||||||
|
|
||||||
(defun tla+/make-link-button (begin end)
|
(defun tla+/make-link-button (begin end)
|
||||||
"Generate button from BEGIN until END
|
"Generate button from BEGIN until END
|
||||||
This function generates a new button starting at BEGIN until END.
|
This function generates a new button starting at BEGIN until END.
|
||||||
The button will execute the `tla+/sany-button-pressed' when a user
|
The button will execute the `tla+/sany-button-pressed' when a user
|
||||||
clicks on it.
|
clicks on it.
|
||||||
"
|
"
|
||||||
(make-button begin end :type 'tla+/sany-button-pressed))
|
(make-button begin end :type 'tla+/sany-button-pressed))
|
||||||
|
|
||||||
(defun tla+/find-error-marks ()
|
(defun tla+/find-error-marks ()
|
||||||
"find error marks reported by SANY.
|
"find error marks reported by SANY.
|
||||||
This function tries to find errors reported by SANY and converts them
|
This function tries to find errors reported by SANY and converts them
|
||||||
into clickable buttons. By clicking on an error, the point will be
|
into clickable buttons. By clicking on an error, the point will be
|
||||||
set to the other-buffer on that particular line and column. Currently
|
set to the other-buffer on that particular line and column. Currently
|
||||||
supported:
|
supported:
|
||||||
line XX, column YY
|
line XX, column YY
|
||||||
|
@ -890,7 +905,7 @@ supported:
|
||||||
XX,YY are natural numbers.
|
XX,YY are natural numbers.
|
||||||
|
|
||||||
The procedure works by:
|
The procedure works by:
|
||||||
1. finding a line that may look like an error message as described
|
1. finding a line that may look like an error message as described
|
||||||
above.
|
above.
|
||||||
2. find the first offset and the last one
|
2. find the first offset and the last one
|
||||||
3. execute the `tla+/make-link-button' function to create a new button
|
3. execute the `tla+/make-link-button' function to create a new button
|
||||||
|
@ -898,7 +913,7 @@ The procedure works by:
|
||||||
(progn
|
(progn
|
||||||
(goto-char (point-min))
|
(goto-char (point-min))
|
||||||
(while (re-search-forward
|
(while (re-search-forward
|
||||||
(concat
|
(concat
|
||||||
"line \\([0-9][0-9]*\\), "
|
"line \\([0-9][0-9]*\\), "
|
||||||
"\\(column\\|col\\) "
|
"\\(column\\|col\\) "
|
||||||
"\\([0-9][0-9]*\\)")
|
"\\([0-9][0-9]*\\)")
|
||||||
|
@ -1002,7 +1017,7 @@ The procedure works by:
|
||||||
:size 18
|
:size 18
|
||||||
:format "Init..............: %v " "Init"))
|
:format "Init..............: %v " "Init"))
|
||||||
(widget-insert "\n")
|
(widget-insert "\n")
|
||||||
|
|
||||||
(setq widget-tlc-next
|
(setq widget-tlc-next
|
||||||
(widget-create 'editable-field
|
(widget-create 'editable-field
|
||||||
:size 18
|
:size 18
|
||||||
|
@ -1028,7 +1043,7 @@ The procedure works by:
|
||||||
(setq widget-tlc-inv widget))
|
(setq widget-tlc-inv widget))
|
||||||
:value '()
|
:value '()
|
||||||
'(editable-field :value "Spec => TypeInv")))
|
'(editable-field :value "Spec => TypeInv")))
|
||||||
|
|
||||||
(widget-insert
|
(widget-insert
|
||||||
"\nList of Constants (CONSTANTS): \n")
|
"\nList of Constants (CONSTANTS): \n")
|
||||||
(setq widget-tlc-constant
|
(setq widget-tlc-constant
|
||||||
|
@ -1053,7 +1068,7 @@ The procedure works by:
|
||||||
(widget-insert "--------------------------------------")
|
(widget-insert "--------------------------------------")
|
||||||
(widget-insert "\nTLC Options\n\n")
|
(widget-insert "\nTLC Options\n\n")
|
||||||
(widget-insert "No Deadlocks.......: " )
|
(widget-insert "No Deadlocks.......: " )
|
||||||
(widget-create 'checkbox
|
(widget-create 'checkbox
|
||||||
:notify
|
:notify
|
||||||
(lambda (&rest ignore)
|
(lambda (&rest ignore)
|
||||||
(let ((cfgtlc
|
(let ((cfgtlc
|
||||||
|
@ -1075,13 +1090,13 @@ The procedure works by:
|
||||||
(tla+/add-option
|
(tla+/add-option
|
||||||
cfgtlc
|
cfgtlc
|
||||||
'tla+-tlc-deadlock
|
'tla+-tlc-deadlock
|
||||||
" ")
|
" ")
|
||||||
))))
|
))))
|
||||||
nil
|
nil
|
||||||
)
|
)
|
||||||
|
|
||||||
(widget-insert "\nSimulation Mode....: ")
|
(widget-insert "\nSimulation Mode....: ")
|
||||||
(widget-create 'checkbox
|
(widget-create 'checkbox
|
||||||
:notify
|
:notify
|
||||||
(lambda (&rest ignore)
|
(lambda (&rest ignore)
|
||||||
(let ((cfgtlc
|
(let ((cfgtlc
|
||||||
|
@ -1204,7 +1219,7 @@ The procedure works by:
|
||||||
"%s\n"
|
"%s\n"
|
||||||
"\n")
|
"\n")
|
||||||
str-confname
|
str-confname
|
||||||
(current-time-string)
|
(current-time-string)
|
||||||
(if (not (string= str-specname "")) ""
|
(if (not (string= str-specname "")) ""
|
||||||
(concat "INIT " str-init "\n"
|
(concat "INIT " str-init "\n"
|
||||||
"NEXT " str-next "\n"))
|
"NEXT " str-next "\n"))
|
||||||
|
@ -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