From a29978acaf93accfe1a759f4d529bf3052b91802 Mon Sep 17 00:00:00 2001 From: Christian Barthel Date: Mon, 6 Jan 2020 22:13:51 +0100 Subject: [PATCH] references, go back to "original window" 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. --- tla+-mode.el | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/tla+-mode.el b/tla+-mode.el index 49fb78c..c8aab99 100644 --- a/tla+-mode.el +++ b/tla+-mode.el @@ -38,7 +38,11 @@ ;; (load "/path/to/tla+-mode.el") ;; and use it with ;; (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: @@ -449,7 +453,8 @@ Operation: (switch-to-buffer sanybuffer) (erase-buffer) (insert output) - (tla+/find-error-marks)))) + (tla+/find-error-marks) + (other-window 1)))) (defun tla+-run-model (cfgfile) "Run the tlc2.TLC Model checker @@ -487,6 +492,7 @@ Note: The TLA+ specification file is a relative path. (switch-to-buffer tlcbuffer) (erase-buffer) (insert output) + (other-window 1) (message (concat "cmd: " cmd)) )))