From 71b6abbf9dba04a782c060958be72d6b167c2cb8 Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Fri, 19 Feb 2021 21:18:08 +0100 Subject: [PATCH] Fix whitespace, add execution cmd message - fixup whitespace globally - dump executed command in notification area --- lisp/tla+-mode.el | 137 +++++++++++++++++++++++----------------------- 1 file changed, 69 insertions(+), 68 deletions(-) diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el index 1592232..9a5df23 100644 --- a/lisp/tla+-mode.el +++ b/lisp/tla+-mode.el @@ -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 ) or with: M-x customize-group 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"))