From 87707476af71147492c584e10975882a533c5c71 Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Mon, 23 Dec 2019 16:50:36 +0100 Subject: [PATCH] add operator insertion menu, ps/pdf conversion, etc. this commit adds - more comments, - change the path to simple binary name. with that, the $PATH variable may be used. Hard coding the path is unnecessarily restrictive. - add dvips and dvipdf convertion (two additional customization parameters define the path to the dvipdf(1) and dvips(1) programs - add action and temporal operators (i.e. functions to insert those symbols). the help text is the one found on the tla+ cheatsheet. - more syntax highlighting for more constants and types --- tla+-mode.el | 182 ++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 158 insertions(+), 24 deletions(-) diff --git a/tla+-mode.el b/tla+-mode.el index 738e6f9..88d33c7 100644 --- a/tla+-mode.el +++ b/tla+-mode.el @@ -20,9 +20,11 @@ ;;; Commentary: - ;; +;; This package defines TLA+ Major Mode to manipulate TLA+ +;; specifications. - ;;; Code: + +;;; Code: (defcustom tla+-mode-hook '() "Normal hook run when entering TLA+ mode." @@ -30,7 +32,7 @@ :options '() :group 'tla+) -(defcustom tla+-java-path "/usr/local/bin/java" +(defcustom tla+-java-path "java" "Path to the `java' program" :type 'file :group 'tla+) @@ -41,12 +43,25 @@ :type 'file :group 'tla+) +(defcustom tla+-dvipdf-path + "dvipdf" + "Path to the `dvipdf' program" + :type 'file + :group 'tla+) +(defcustom tla+-dvips-path + "dvips" + "Path to the `dvips' program" + :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))) (set-keymap-parent map lisp-mode-shared-map) (define-key map "\e\t" 'ispell-complete-word) @@ -55,6 +70,73 @@ (bindings--define-key map [menu-bar tla+] (cons "TLA+" menu-map)) + ;; Operators + (bindings--define-key menu-map [operator] + (cons "Insert Operator.." operator-map)) + + ;; Action Operators + (bindings--define-key operator-map [action-operator] + (cons "Action Operator" action-operator-map)) + + (bindings--define-key + 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 + :help "A \\/ (e' = e)")) + + (bindings--define-key + action-operator-map [nonstutter-operator] + '(menu-item "<>_e" tla+-operator-nonstutter + :help "A /\ (e' \\= e)")) + + (bindings--define-key + 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] + '(menu-item "UNCHANGED e" tla+-operator-unchanged + :help "e = e'")) + + (bindings--define-key + action-operator-map [composition-operator] + '(menu-item "A \\cdot B" tla+-operator-composition + :help "Composition of actions")) + + ;; Temporal operators: + (bindings--define-key operator-map [temporal-operator] + (cons "Temporal Operator" temporal-operator-map)) + + (bindings--define-key + 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] + '(menu-item "<>F" tla+-operator-eventually + :help "F is eventually true")) + + (bindings--define-key + 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] + '(menu-item "SF_e(A)" tla+-operator-strongfairness + :help "Strong fairness for action A")) + + (bindings--define-key + 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)) @@ -81,7 +163,7 @@ '(menu-item "Run Syntax Checker" tla+-run-sany :help "Run SANY2 " - "(parser and syntax checker for TLA+ specifications.) ")) + "(parser/syntax checker for TLA+ specifications.) ")) (bindings--define-key map [menu-bar tla+ tla+-create-module] '(menu-item "Create new Module" tla+-create-module @@ -93,21 +175,22 @@ (defconst tla+-font-lock-keywords (list - '("\\<\\(MODULE\\|CONSTANT\\|UNCHANGED\\|VARIABLE\\|THEOREM\\|EXCEPT\\|EXTENDS\\)\\>" + '("\\<\\(MODULE\\|CONSTANTS?\\|UNCHANGED\\|VARIABLES?\\|THEOREM\\|INSTANCE\\|LOCAL\\|ASUME\\|EXCEPT\\|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) '("\\\\\\*.*$" . font-lock-comment-face) '("(\\*.*\\*)" . font-lock-comment-face) '("\\('\\w*'\\)" . font-lock-variable-name-face) - "Highlighting for TLA+ Keywords.")) + "Highlighting for TLA+ Operators, Keywords etc.")) ;;;###autoload (add-to-list 'auto-mode-alist '("\\.tla\\'" . tla+-mode)) ;;;###autoload (define-derived-mode tla+-mode nil "TLA+" - "Major mode for editing text written for humans to read. -In this mode, paragraphs are delimited only by blank or white lines. -You can thus get the full benefit of adaptive filling - (see the variable `adaptive-fill-mode'). + "Major mode for editing TLA+ specifications. +In this mode, syntax highlighting is activated for TLA+ specification +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 @@ -120,13 +203,14 @@ Turning on Text mode runs the normal hook `text-mode-hook'." (interactive) (insert (concat - "------------------- MODULE ......... -----------------------\n" - "EXTENDS Naturals, ...\n" - "VARIABLE ..\n" - "------------------------------------------------------------\n" - "============================================================\n" - "\\* Modification History\n" - "\\* Created " (current-time-string) " by " user-full-name "\n"))) + "------------------- MODULE ......... -----------------------\n" + "EXTENDS Naturals, ...\n" + "VARIABLE ..\n" + "------------------------------------------------------------\n" + "============================================================\n" + "\\* Modification History\n" + "\\* Created " + (current-time-string) " by " user-full-name "\n"))) (defun tla+-run-sany () @@ -152,9 +236,44 @@ Turning on Text mode runs the normal hook `text-mode-hook'." (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 () + (interactive) (insert " []F")) + +(defun tla+-operator-eventually () + (interactive) (insert " <>F")) + +(defun tla+-operator-weakfairness () + (interactive) (insert " WF_e(A)")) + +(defun tla+-operator-strongfairness () + (interactive) (insert " SF_e(A)")) + +(defun tla+-operator-leadsto () + (interactive) (insert " F~>G ")) + +(defun tla+-operator-stutter () + (interactive) (insert " [A]_e")) + +(defun tla+-operator-primed () + (interactive) (insert " e'")) + + +(defun tla+-operator-nonstutter () + (interactive) (insert " <>_e")) + +(defun tla+-operator-enabled () + (interactive) (insert " ENABLED A")) + +(defun tla+-operator-unchanged () + (interactive) (insert " UNCHANGED e")) + +(defun tla+-operator-unchanged () + (interactive) (insert " A \\cdot B")) + (defun tla+-run-tlatex (type) "TODO: jump to line.." (interactive @@ -168,16 +287,31 @@ Turning on Text mode runs the normal hook `text-mode-hook'." " -cp " tla+-tlatools-path " tla2tex.TLA " - filename)))) - type)) + 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)) + ((eq type 'ps) + (shell-command convert2ps))) + type))) ;; (save-excursion ;; (split-window-below) ;; (other-window 1) ;; (switch-to-buffer sanybuffer) ;; (insert output)))) -(defun tla+-run-tlatex-pdf () (tla+-run-tlatex 'pdf)) -(defun tla+-run-tlatex-dvi () (tla+-run-tlatex 'dvi)) -(defun tla+-run-tlatex-ps () (tla+-run-tlatex 'ps)) +(defun tla+-run-tlatex-pdf () + (interactive) (tla+-run-tlatex 'pdf)) +(defun tla+-run-tlatex-dvi () + (interactive) (tla+-run-tlatex 'dvi)) +(defun tla+-run-tlatex-ps () + (interactive) (tla+-run-tlatex 'ps)) (provide 'tla+-mode)