From 5f04536a3579fe889260cfd328b053173e56ef35 Mon Sep 17 00:00:00 2001
From: Christian Barthel <bch@online.de>
Date: Tue, 18 Feb 2020 22:12:12 +0100
Subject: [PATCH] tlc settings, tlc error buttons

- compilation output buffers (sany, tlc) store
  the name of the TLA+ file.
  this can be used to jump back to the buffer
  if the tla+/find-error-marks highlights
  "line:column" markers.
- use tla+/find-error-marks with the TLC output
- add additional tlc global setting
---
 tla+-mode.el | 68 ++++++++++++++++++++++++++++++++++++++++++----------
 1 file changed, 55 insertions(+), 13 deletions(-)

diff --git a/tla+-mode.el b/tla+-mode.el
index dd6d030..e86538c 100644
--- a/tla+-mode.el
+++ b/tla+-mode.el
@@ -1,4 +1,4 @@
-;; Copyright (C) 2019  Christian Barthel <bch@online.de>
+;; Copyright (C) 2019-2020  Christian Barthel <bch@online.de>
 
 ;; Author: Christian Barthel
 ;; Keywords: TLA+
@@ -92,6 +92,37 @@
   :type 'string
   :group 'tla+)
 
+(defcustom tla+-tlc-deadlock
+  " -deadlock "
+  "Tell `TLC' not to check for deadlocks"
+  :type 'string
+  :group 'tla+)
+
+(defcustom tla+-tlc-simulate
+  "  "
+  "Tell `TLC' to do simulation (randomly chosen behaviors) (-simulate)"
+  :type 'string
+  :group 'tla+)
+
+(defcustom tla+-tlc-depth
+  " -depth 100 "
+  "Tell `TLC' to do max. X steps (default: 100)"
+  :type 'string
+  :group 'tla+)
+
+(defcustom tla+-tlc-coverage
+  "  "
+  "Tell `TLC' to print coverage every X minutes: -coverage X"
+  :type 'string
+  :group 'tla+)
+
+(defcustom tla+-tlc-workers
+  " -workers 1 "
+  "Tell `TLC' how many threads to generate."
+  :type 'string
+  :group 'tla+)
+
+
 
 
 ;; -------------------------------------------------------------------
@@ -461,7 +492,9 @@ Operation:
    `tla+/find-error-marks' function."
   (interactive)
   (let* ((filename (buffer-file-name))
-         (sanybuffer (get-buffer-create "*tla2sany.SANY*"))
+         (sanybuffer
+	  (get-buffer-create
+	   (format "*tla2sany.SANY* [%s]" (buffer-name))))
          (output   (shell-command-to-string (concat
                                    tla+-java-path
                                    " -cp "
@@ -496,7 +529,8 @@ Note: The TLA+ specification file is a relative path.
 	     (file-name-base (buffer-file-name))
 	     ".cfg" ))))
   (let* ((filename (buffer-file-name))
-	 (tlcbuffer (get-buffer-create "*tlc2.TLC*"))
+	 (tlcbuffer (get-buffer-create
+		     (format "*tlc2.TLC* [%s]" (buffer-name))))
 	 ;; XXX: tlc2.TLC -config /full/path/to/TLA.cfg TLA.tla
 	 ;;  not sure why the tla file itself should not be a
 	 ;;  full path?
@@ -504,6 +538,11 @@ Note: The TLA+ specification file is a relative path.
 	 (cmd (concat
 	       tla+-java-path " -cp " tla+-tlatools-path
 	       " tlc2.TLC "
+	       tla+-tlc-deadlock " "
+	       tla+-tlc-simulate " "
+	       tla+-tlc-depth " "
+	       tla+-tlc-coverage " "
+	       tla+-tlc-workers " "	       
 	       " -config " cfgfile " "
 	       finame))
 	 (output (shell-command-to-string cmd)))
@@ -513,8 +552,10 @@ Note: The TLA+ specification file is a relative path.
       (switch-to-buffer tlcbuffer)
       (erase-buffer)
       (insert output)
+      (tla+/find-error-marks)
       (other-window 1)
-      (message  (concat "cmd: " cmd))
+      ;(message "marked")
+      ;(message  (concat "cmd: " cmd))
       )))
 
 
@@ -532,7 +573,8 @@ was not 0), an error message will be printed.
   (let* ((filename (buffer-file-name))
 	 (oldfile (replace-regexp-in-string
 		   ".tla$" ".old" filename))
-	 (pcalbuf (get-buffer-create "*pcal.trans*"))
+	 (pcalbuf (get-buffer-create
+		   (format "*pcal.trans* [%s]" (buffer-name))))
 	 (cmd (concat 
 	       tla+-java-path " -cp " tla+-tlatools-path
 	       " pcal.trans "filename ))
@@ -696,6 +738,11 @@ Steps done by this function:
 5. goto line and column.
 "
   (let* ((pos (point))
+	 (buffername
+	  (replace-regexp-in-string
+	   "\\*.*\\* \\[\\(.*\\)\\]"
+	   "\\1"
+	   (buffer-name)))
          (the-button (button-at pos))
          (text (button-label the-button))
          (s (string-match
@@ -708,15 +755,10 @@ Steps done by this function:
          (col (string-to-number (match-string 3 text))))
     ;(message (format "Button pressed: %s" text))
     (progn
-      ;(switch-to-buffer (other-buffer))
-      (other-window 1)
-      ;(switch-to-buffer (other-buffer))
-      ;(switch-to-buffer-other-window (current-buffer))
+      (switch-to-buffer-other-window buffername)
       (goto-char (point-min))
       (goto-line line)
-      (forward-char col)
-      ;(switch-to-buffer (other-buffer))
-      ;(message "%s" (buffer-name))
+      (forward-char (- col 1))
     )))
 
 (defun tla+/make-link-button (begin end)
@@ -756,7 +798,7 @@ The procedure works by:
              (colnum (match-beginning 3))
              (rend (+ colnum (- (length (int-to-string colnum)) 0)))
              )
-	;(message "%s %s" linenum colnum)
+	(message "%s %s" linenum colnum)
 	;(message "%d %d" rstart rend)
         (tla+/make-link-button rstart rend)
         ))))