bch/tlamode
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Fix whitespace, add execution cmd message

Browse Source 
- fixup whitespace globally
- dump executed command in notification area
This commit is contained in:
Christian Barthel 2021-02-19 21:18:08 +01:00
parent 78a196b94d
commit 71b6abbf9d
1 changed files with 69 additions and 68 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

137
lisp/tla+-mode.el
View File

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