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)