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

comments, modul operators, mark error messages 

- add comments
- add keybord shortcuts
- add modul operators (from naturals, sequences)
- add functions to mark error messages in the SANY
  check buffer.
This commit is contained in:
Christian Barthel 2019-12-26 08:16:03 +01:00
parent 87707476af
commit c58bbb6671
1 changed files with 383 additions and 75 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

458
tla+-mode.el
View File

@ -1,24 +1,24 @@
;; Copyright (C) 2019 Christian Barthel <bch@online.de>
;; Copyright (C) 2019 Christian Barthel <bch@online.de>
;; 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 "<<A>>_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)