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

references, go back to "original window"

Browse Source 
this commit adds some references to get the
tlatoolbox.jar.
i also changed the behavior of running sany
and tlc slightly: if a new window pops up,
i switch back to the tla buffer.  a simple
c-x 1 gets rid of the message buffer.
This commit is contained in:
Christian Barthel 2020-01-06 22:13:51 +01:00
parent 30d6a1b7ee
commit a29978acaf
1 changed files with 8 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
tla+-mode.el
View File

@ -38,7 +38,11 @@
;; (load "/path/to/tla+-mode.el") ;; (load "/path/to/tla+-mode.el")
;; and use it with ;; and use it with
;; (require tla+-mode) ;; (require tla+-mode)
;;
;; Getting, and Using the tlatoolbox:
;; https://tla.msr-inria.inria.fr/tlatoolbox/dist/
;; https://lamport.azurewebsites.net/tla/tools.html
;; https://lamport.azurewebsites.net/tla/standalone-tools.html
;;; Code: ;;; Code:
@ -449,7 +453,8 @@ Operation:
(switch-to-buffer sanybuffer) (switch-to-buffer sanybuffer)
(erase-buffer) (erase-buffer)
(insert output) (insert output)
(tla+/find-error-marks)))) (tla+/find-error-marks)
(other-window 1))))
(defun tla+-run-model (cfgfile) (defun tla+-run-model (cfgfile)
"Run the tlc2.TLC Model checker "Run the tlc2.TLC Model checker
@ -487,6 +492,7 @@ Note: The TLA+ specification file is a relative path.
(switch-to-buffer tlcbuffer) (switch-to-buffer tlcbuffer)
(erase-buffer) (erase-buffer)
(insert output) (insert output)
(other-window 1)
(message (concat "cmd: " cmd)) (message (concat "cmd: " cmd))
))) )))