diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el index 6103816..08577c5 100644 --- a/lisp/tla+-mode.el +++ b/lisp/tla+-mode.el @@ -503,9 +503,9 @@ Configuration: M-x describe-variable Getting, and Using the tlatoolbox: -[1] https://tla.msr-inria.inria.fr/tlatoolbox/dist/ -[2] https://lamport.azurewebsites.net/tla/tools.html -[3] https://lamport.azurewebsites.net/tla/standalone-tools.html +[1] +[2] +[3] \\{tla+-mode-map} Turning on Text mode runs the normal hook `text-mode-hook'." (setq-local font-lock-defaults @@ -789,11 +789,7 @@ The function executes one or two shell commands synchronously." ((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 () "Create PDF file from TLA+ Specification. @@ -1050,15 +1046,17 @@ The procedure works by: :notify (lambda (&rest ignore) (let ((cfgtlc - (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" - "\\1tlcopt" - (buffer-name)))) + (replace-regexp-in-string + ".*\\[\\(.*\\)\\].*" + "\\1tlcopt" + (buffer-name)))) (tla+/read-options cfgtlc) (let ((value (cdr (assoc 'tla+-tlc-deadlock tla+-option-list)))) - (if (or (equal nil value) (string= value " ")) + (if (or (equal nil value) + (string= value " ")) (tla+/add-option cfgtlc 'tla+-tlc-deadlock @@ -1076,15 +1074,17 @@ The procedure works by: :notify (lambda (&rest ignore) (let ((cfgtlc - (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" - "\\1" - (buffer-name)))) + (replace-regexp-in-string + ".*\\[\\(.*\\)\\].*" + "\\1" + (buffer-name)))) (tla+/read-options cfgtlc) (let ((value (cdr (assoc 'tla+-tlc-simulate tla+-option-list)))) - (if (or (equal value nil) (string= value " ")) + (if (or (equal value nil) + (string= value " ")) (tla+/add-option cfgtlc 'tla+-tlc-simulate @@ -1105,9 +1105,10 @@ The procedure works by: :notify (lambda (widget &rest ignore) (let ((cfgtlc - (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" - "\\1" - (buffer-name)))) + (replace-regexp-in-string + ".*\\[\\(.*\\)\\].*" + "\\1" + (buffer-name)))) (tla+/add-option cfgtlc 'tla+-tlc-depth (format " -depth %s " @@ -1127,9 +1128,10 @@ The procedure works by: :notify (lambda (widget &rest ignore) (let ((cfgtlc - (replace-regexp-in-string ".*\\[\\(.*\\)\\].*" - "\\1" - (buffer-name)))) + (replace-regexp-in-string + ".*\\[\\(.*\\)\\].*" + "\\1" + (buffer-name)))) (tla+/add-option cfgtlc 'tla+-tlc-workers (format " -workers %s " @@ -1146,15 +1148,16 @@ The procedure works by: :notify (lambda (&rest ignore) (let* - ((config-buffer - (get-buffer-create - (replace-regexp-in-string + ((confname + (replace-regexp-in-string ".tla$" ".cfg" (replace-regexp-in-string "\\*TLC Configuration\\* \\[\\(.*\\)\\]" "\\1" (buffer-name)) - ))) + )) + (config-buffer (get-buffer-create confname)) + (config-buffer-file-name (buffer-file-name config-buffer)) (str-confname (widget-value widget-tlc-confname)) (str-specname (widget-value widget-tlc-specname)) (str-init (widget-value widget-tlc-init)) @@ -1164,13 +1167,21 @@ The procedure works by: (lst-const (widget-value widget-tlc-constant)) (lst-constraint (widget-value widget-tlc-constraint))) (progn + (if (and confname + (file-exists-p confname)) + (rename-file confname + (concat confname ".old." + (number-to-string + (nth 1 (current-time))) + ))) (switch-to-buffer config-buffer) + (erase-buffer) (tla+-mode) (insert (format (concat "\\* -*- mode: tla+; -*-\n" "\\* TLA+ Config %s\n" - "\\* XXX date/time\n" + "\\* Created %s\n" "%s\n" "\\* properties\n" "%s\n" @@ -1182,6 +1193,7 @@ The procedure works by: "%s\n" "\n") str-confname + (current-time-string) (if (not (string= str-specname "")) "" (concat "INIT " str-init "\n" "NEXT " str-next "\n")) diff --git a/org/Test.org b/org/Test.org new file mode 100644 index 0000000..0ba7ea5 --- /dev/null +++ b/org/Test.org @@ -0,0 +1,43 @@ +* This is an Org file +** TLA+ with Org +This is an attempt to combine Org-Mode Babel with TLA+. + +Keyboard Shortcuts: + +| Keystroke | Description | +|-----------+-------------------------| +| c-c c-t c | SANY Syntactic Analyzer | +| c-c c-t e | Export DVI | +| c-c c-t o | Open DVI file | +| c-c c-t m | run TLC model checker | +| c-c c-t p | run PlusCal Translator | + +** Modul1 with descriptions + +uyam erat, sed diam voluptua. At *vero* eos et accusam et justo duo +dolores et ea rebum. _Stet_ clita kasd gubergren, no sea takimata +sanctus est Lorem ipsum dolor sit amet. + +- Unordered List + - a + - b +- Unordered + +Use: ~org-babel-tangle~ to export the module above: + +#+BEGIN_SRC tla+ :tangle TestModul.tla + ------------------- MODULE TestModul ----------------------- + EXTENDS Naturals + VARIABLE hr + ------------------------------------------------------------ + Init == hr \in (1..12) + Next == hr' = IF hr = 12 THEN + 1 + ELSE + hr + 1 + ------------------------------------------------------------ + Spec == Init /\ [][Next]_hr + ============================================================ + \* Modification History + \* Created Mon Aug 3 03:46:40 2020 by Christian Barthel +#+END_SRC