diff --git a/tla+-mode.el b/tla+-mode.el index 88d33c7..a440a4c 100644 --- a/tla+-mode.el +++ b/tla+-mode.el @@ -1,24 +1,24 @@ - ;; Copyright (C) 2019 Christian Barthel +;; Copyright (C) 2019 Christian Barthel - ;; Author: Christian Barthel - ;; Keywords: TLA+ +;; Author: Christian Barthel +;; Keywords: TLA+ - ;; This file is free software; you can redistribute it and/or modify - ;; it under the terms of the GNU General Public License as published by - ;; the Free Software Foundation; either version 2, or (at your option) - ;; any later version. +;; This file is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation; either version 2, or (at your option) +;; any later version. - ;; This file is distributed in the hope that it will be useful, - ;; but WITHOUT ANY WARRANTY; without even the implied warranty of - ;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - ;; GNU General Public License for more details. +;; This file is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. - ;; You should have received a copy of the GNU General Public License - ;; along with GNU Emacs; see the file COPYING. If not, write to - ;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330, - ;; Boston, MA 02111-1307, USA. +;; You should have received a copy of the GNU General Public License +;; along with GNU Emacs; see the file COPYING. If not, write to +;; the Free Software Foundation, Inc., 59 Temple Place - Suite 330, +;; Boston, MA 02111-1307, USA. - ;;; Commentary: +;;; Commentary: ;; This package defines TLA+ Major Mode to manipulate TLA+ ;; specifications. @@ -26,6 +26,10 @@ ;;; Code: + +;; ------------------------------------------------------------------- +;; Customization variables: + (defcustom tla+-mode-hook '() "Normal hook run when entering TLA+ mode." :type 'hook @@ -55,21 +59,185 @@ :type 'file :group 'tla+) + +;; ------------------------------------------------------------------------------- (defvar tla+-mode-map (let ((map (make-sparse-keymap)) (menu-map (make-sparse-keymap "TLA+")) + (operator-map (make-sparse-keymap)) + (action-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-sequences-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 c") 'tla+-run-sany) ;; Main TLA+ Menu: (bindings--define-key map [menu-bar tla+] (cons "TLA+" menu-map)) + ;; Modul Operators + (bindings--define-key menu-map [modul-operators] + (cons "Insert Modul Operator.." modul-operators)) + + ;; Naturals Operators + (bindings--define-key modul-operators + [modul-naturals-operator] + (cons "Naturals" modul-naturals-operators)) + + (bindings--define-key + modul-naturals-operators [add-nat] + '(menu-item "+" + (lambda () (interactive) + (insert "+")) + :help "Addition")) + + (bindings--define-key + modul-naturals-operators [sub-nat] + '(menu-item "-" + (lambda () (interactive) + (insert "-") + (backward-char 2)) + :help "Subtraction")) + + (bindings--define-key + modul-naturals-operators [mult-nat] + '(menu-item "*" + (lambda () (interactive) + (insert "*")) + :help "Multiplication")) + + (bindings--define-key + modul-naturals-operators [div-nat] + '(menu-item "/" + (lambda () (interactive) + (insert "/")) + :help "Division")) + + (bindings--define-key + modul-naturals-operators [exp-nat] + '(menu-item "^" + (lambda () (interactive) + (insert "^")) + :help "Exponentiation")) + + (bindings--define-key + modul-naturals-operators [ft-nat] + '(menu-item ".." + (lambda () (interactive) + (insert "..")) + :help "From..To")) + + (bindings--define-key + modul-naturals-operators [div2-nat] + '(menu-item "\\div" + (lambda () (interactive) + (insert "\div")) + :help "Integer Division")) + + + (bindings--define-key + modul-naturals-operators [mod-nat] + '(menu-item "%" + (lambda () (interactive) + (insert "%")) + :help "Modulo")) + + + (bindings--define-key + modul-naturals-operators [leq-nat] + '(menu-item "\\leq" + (lambda () (interactive) + (insert "\\leq")) + :help "Lower Equal")) + + (bindings--define-key + modul-naturals-operators [geq-nat] + '(menu-item "\\geq" + (lambda () (interactive) + (insert "\\geq")) + :help "Greater Equal")) + + (bindings--define-key + modul-naturals-operators [lt-nat] + '(menu-item "<" + (lambda () (interactive) + (insert "<")) + :help "Lower than")) + + (bindings--define-key + modul-naturals-operators [gt-nat] + '(menu-item ">" + (lambda () (interactive) + (insert ">")) + :help "Greater than")) + + + ;; Sequence Operators + (bindings--define-key modul-operators + [modul-sequences-operator] + (cons "Sequences" modul-sequences-operators)) + + (bindings--define-key + modul-sequences-operators [seq-s] + '(menu-item "Seq(S)" + (lambda () (interactive) + (insert "Seq(S)") + (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)" + (lambda () (interactive) + (insert "Head(s)") + (backward-char 2)) + :help "Head element of sequence `s'")) + + (bindings--define-key + modul-sequences-operators [tail-s] + '(menu-item "Tail(s)" + (lambda () (interactive) + (insert "Tail(s)") + (backward-char 2)) + :help "Tail sequence of sequence `s'")) + + (bindings--define-key + modul-sequences-operators [append-s] + '(menu-item "Append(s,e)" + (lambda () (interactive) + (insert "Tail(S)") + (backward-char 2)) + :help "Tail sequence of sequence `S'")) + + (bindings--define-key + modul-sequences-operators [circ-s] + '(menu-item "s \\circ t" + (lambda () (interactive) + (insert "s \\circ t") + (backward-char 2)) + :help "concatenation of sequence s and t")) + + (bindings--define-key + modul-sequences-operators [len-s] + '(menu-item "Len(s)" + (lambda () (interactive) + (insert "Len(s)") + (backward-char 2)) + :help "length of sequence s")) + + ;; Operators (bindings--define-key menu-map [operator] (cons "Insert Operator.." operator-map)) @@ -79,32 +247,32 @@ (cons "Action Operator" action-operator-map)) (bindings--define-key - action-operator-map [primed-operator] + 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] + action-operator-map [stutter-operator] '(menu-item "[A]_e" tla+-operator-stutter :help "A \\/ (e' = e)")) (bindings--define-key - action-operator-map [nonstutter-operator] + action-operator-map [nonstutter-operator] '(menu-item "<>_e" tla+-operator-nonstutter - :help "A /\ (e' \\= e)")) + :help "A /\\ (e' \\\\ = e)")) (bindings--define-key - action-operator-map [enabled-operator] + action-operator-map [enabled-operator] '(menu-item "ENABLED A" tla+-operator-enabled :help "An A step is possible")) (bindings--define-key - action-operator-map [unchanged-operator] + action-operator-map [unchanged-operator] '(menu-item "UNCHANGED e" tla+-operator-unchanged :help "e = e'")) (bindings--define-key - action-operator-map [composition-operator] + action-operator-map [composition-operator] '(menu-item "A \\cdot B" tla+-operator-composition :help "Composition of actions")) @@ -113,32 +281,33 @@ (cons "Temporal Operator" temporal-operator-map)) (bindings--define-key - temporal-operator-map [always-temporal-operator] + temporal-operator-map [always-temporal-operator] '(menu-item "[]F" tla+-operator-alwaystrue :help "F is always true")) (bindings--define-key - temporal-operator-map [eventually-temporal-operator] + temporal-operator-map [eventually-temporal-operator] '(menu-item "<>F" tla+-operator-eventually :help "F is eventually true")) (bindings--define-key - temporal-operator-map [wf-temporal-operator] + temporal-operator-map [wf-temporal-operator] '(menu-item "WF_e(A)" tla+-operator-weakfairness :help "Weak fairness for action A")) (bindings--define-key - temporal-operator-map [sf-temporal-operator] + temporal-operator-map [sf-temporal-operator] '(menu-item "SF_e(A)" tla+-operator-strongfairness :help "Strong fairness for action A")) (bindings--define-key - temporal-operator-map [leadsto-temporal-operator] + 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 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 @@ -161,24 +330,24 @@ (bindings--define-key map [menu-bar tla+ tla+-run-sany] '(menu-item "Run Syntax Checker" tla+-run-sany - :help - "Run SANY2 " - "(parser/syntax checker for TLA+ specifications.) ")) + :help + "Run SANY2 " + "(syntax checker for TLA+ specifications) ")) (bindings--define-key map [menu-bar tla+ tla+-create-module] '(menu-item "Create new Module" tla+-create-module - :help "Create a new TLA+ Module")) - (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator) + :help "Create a new TLA+ Module")) + (bindings--define-key map [menu-bar tla+ sep] menu-bar-separator) map) "Keymap for `tla+-mode'.") (defconst tla+-font-lock-keywords (list - '("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|INSTANCE\\|LOCAL\\|ASUME\\|EXCEPT\\|EXTENDS?\\)\\>" + '("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|LOCAL\\|ASUME\\|EXTENDS?\\)\\>" . font-lock-builtin-face) '("\\<\\(TRUE\\|FALSE\\|OTHER\\|BOOLEAN\\)\\>" . font-lock-type-face) - '("\\<\\(CONSTANT\\|SUBSET\\|ENABLED\\|UNCHANGED\\|UNION\\|DOMAIN\\|EXCEPT\\|IF\\|THEN\\|ELSE\\|CHOOSE\\)\\>" . font-lock-keyword-face) + '("\\<\\(CONSTANT\\|SUBSET\\|ENABLED\\|UNCHANGED\\|INSTANCE\\|WITH\\|EXCEPT\\|UNION\\|DOMAIN\\|EXCEPT\\|IF\\|THEN\\|ELSE\\|CHOOSE\\)\\>" . font-lock-keyword-face) '("\\\\\\*.*$" . font-lock-comment-face) '("(\\*.*\\*)" . font-lock-comment-face) '("\\('\\w*'\\)" . font-lock-variable-name-face) @@ -194,50 +363,74 @@ files. Various operators can be inserted by `tla+-operator-NAME'. \\{text-mode-map} Turning on Text mode runs the normal hook `text-mode-hook'." (setq-local font-lock-defaults - '(tla+-font-lock-keywords)) + '(tla+-font-lock-keywords)) (setq-local text-mode-variant t) (setq-local comment-start "\\* ") (setq-local require-final-newline mode-require-final-newline)) + (defun tla+-create-module () + "Insert the base template for a new Module. +A new module will be created with the typical structure of a TLA+ +specification file." (interactive) - (insert - (concat - "------------------- MODULE ......... -----------------------\n" - "EXTENDS Naturals, ...\n" - "VARIABLE ..\n" - "------------------------------------------------------------\n" - "============================================================\n" - "\\* Modification History\n" - "\\* Created " - (current-time-string) " by " user-full-name "\n"))) + (let ((modulename + (concat (file-name-base (buffer-file-name))))) + (insert + (concat + "------------------- MODULE " + modulename + " -----------------------\n" + "EXTENDS Naturals, ...\n" + "VARIABLE ..\n" + "------------------------------------------------------------\n" + "============================================================\n" + "\\* Modification History\n" + "\\* Created " + (current-time-string) " by " user-full-name "\n")))) (defun tla+-run-sany () - "TODO: jump to line.." + "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 +directly go to the error line. + +Operation: +1. execute the tla2sany.SANY program +2. the output of the shell-command is inserted into a newly + created buffer +3. errors are converted into clickable buttons by using the + `tla+/find-error-marks' function." (interactive) (let* ((filename (buffer-file-name)) - (sanybuffer (get-buffer-create "*tla2sany.SANY*")) - (output (shell-command-to-string (concat - tla+-java-path - " -cp " - tla+-tlatools-path - " tla2sany.SANY " - filename)))) + (sanybuffer (get-buffer-create "*tla2sany.SANY*")) + (output (shell-command-to-string (concat + tla+-java-path + " -cp " + tla+-tlatools-path + " tla2sany.SANY " + filename)))) (save-excursion (split-window-below) (other-window 1) (switch-to-buffer sanybuffer) (erase-buffer) - (insert output)))) + (insert output) + (tla+/find-error-marks)))) (defun tla+-open-dvi (buffername) + "Function to open a DVI file. +This function starts the `xdvi' utility and opens the TLA+ +specification file as DVI. It must be created beforehand +with the `tla+-run-tlatex-dvi'. +" (interactive "b") (save-excursion (switch-to-buffer buffername) (let* ((filename (buffer-file-name)) - (dviname (replace-regexp-in-string - ".tla$" ".dvi" filename))) + (dviname (replace-regexp-in-string + ".tla$" ".dvi" filename))) (shell-command (concat "xdvi " dviname " &"))))) (defun tla+-operator-alwaystrue () @@ -269,37 +462,46 @@ Turning on Text mode runs the normal hook `text-mode-hook'." (interactive) (insert " ENABLED A")) (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. " (interactive) (insert " UNCHANGED e")) -(defun tla+-operator-unchanged () +(defun tla+-operator-cdot () + "insert operator A \\cdot B +A \\cdot B describes the composition of actions A, B." (interactive) (insert " A \\cdot B")) (defun tla+-run-tlatex (type) - "TODO: jump to line.." + "Run TLaTeX and generate DVI, PDF or PS file. +This function runs `pdflatex(1)' and geneartes a DVI file which can +be viewed with `xdvi'. If TYPE is 'pdf or 'ps, a PDF or PostScript +file will be generated as well. +The function executes one or two shell commands synchronously." (interactive (list (completing-read "Format: " '(("pdf" 1) ("dvi" 2) ("ps" 3)) nil t ""))) (let* ((filename (buffer-file-name)) - (output (shell-command (concat - tla+-java-path - " -cp " - tla+-tlatools-path - " tla2tex.TLA " - filename))) - (dvipath (replace-regexp-in-string - ".tla$" ".dvi" filename)) - (convert2pdf (concat - tla+-dvipdf-path " " dvipath)) - (convert2ps (concat - tla+-dvips-path " " dvipath))) + (output (shell-command (concat + tla+-java-path + " -cp " + tla+-tlatools-path + " tla2tex.TLA " + filename))) + (dvipath (replace-regexp-in-string + ".tla$" ".dvi" filename)) + (convert2pdf (concat + tla+-dvipdf-path " " dvipath)) + (convert2ps (concat + tla+-dvips-path " " dvipath))) (progn (cond ((eq type 'pdf) - (shell-command convert2pdf)) + (shell-command convert2pdf)) ((eq type 'ps) - (shell-command convert2ps))) + (shell-command convert2ps))) type))) ;; (save-excursion ;; (split-window-below) @@ -308,10 +510,116 @@ Turning on Text mode runs the normal hook `text-mode-hook'." ;; (insert output)))) (defun tla+-run-tlatex-pdf () + "Create PDF file from TLA+ Specification. +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'" (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'" (interactive) (tla+-run-tlatex 'ps)) + + +;; internal functions: + +(define-button-type + 'tla+/sany-button-pressed + 'action 'tla+/sany-button-pressed + 'follow-link t + 'help-echo "Goto Source" + 'help-args "test") + +;; example: (make-button 1 12 :type 'custom-button) + +(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 +window and going to the line mentioned in the error message. +The parameter BUTTON is currently unused. + +Steps done by this function: +1. get the button at the current position of the `point' +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 + specification where SANY was executed. +5. goto line and column. +" + (let* ((pos (point)) + (the-button (button-at pos)) + (text (button-label the-button)) + (s (string-match + (concat + "line \\([0-9][0-9]*\\)," ; line XYZ + "\\(column\\|col\\) " ; "column" or "col" + "\\([0-9][0-9]*\\)" ; XYZ + text)) + (line (string-to-number (match-string 1 text))) + (col (string-to-number (match-string 3 text))) + ) + ;(message (format "Button pressed: %s" text)) + (progn + ;(switch-to-buffer (other-buffer)) + (other-window 1) + ;(switch-to-buffer (other-buffer)) + ;(switch-to-buffer-other-window (current-buffer)) + (goto-char (point-min)) + (goto-line line) + (forward-char col) + ;(switch-to-buffer (other-buffer)) + ;(message "%s" (buffer-name)) + ))) + +(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 +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 +set to the other-buffer on that particular line and column. Currently +supported: + line XX, column YY + line XX, col YY +XX,YY are natural numbers. + +The procedure works by: +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 +" + (progn + (goto-char (point-min)) + (while (re-search-forward + (concat + "line \\([0-9][0-9]*\\), " + "\\(column\\|col\\) " + "\\([0-9][0-9]*\\)") + (point-max) t) + (let* ((rstart (match-beginning 0)) + (linenum (match-beginning 1)) + (colnum (match-beginning 3)) + (rend (+ colnum (- (length (int-to-string colnum)) 0))) + ) + ;(message "%s %s" linenum colnum) + (tla+/make-link-button rstart rend) + )))) + + + (provide 'tla+-mode)