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
This commit is contained in:
parent
1522267517
commit
5f04536a35
68
tla+-mode.el
68
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
|
;; Author: Christian Barthel
|
||||||
;; Keywords: TLA+
|
;; Keywords: TLA+
|
||||||
|
@ -92,6 +92,37 @@
|
||||||
:type 'string
|
:type 'string
|
||||||
:group 'tla+)
|
: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."
|
`tla+/find-error-marks' function."
|
||||||
(interactive)
|
(interactive)
|
||||||
(let* ((filename (buffer-file-name))
|
(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
|
(output (shell-command-to-string (concat
|
||||||
tla+-java-path
|
tla+-java-path
|
||||||
" -cp "
|
" -cp "
|
||||||
|
@ -496,7 +529,8 @@ Note: The TLA+ specification file is a relative path.
|
||||||
(file-name-base (buffer-file-name))
|
(file-name-base (buffer-file-name))
|
||||||
".cfg" ))))
|
".cfg" ))))
|
||||||
(let* ((filename (buffer-file-name))
|
(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
|
;; XXX: tlc2.TLC -config /full/path/to/TLA.cfg TLA.tla
|
||||||
;; not sure why the tla file itself should not be a
|
;; not sure why the tla file itself should not be a
|
||||||
;; full path?
|
;; full path?
|
||||||
|
@ -504,6 +538,11 @@ Note: The TLA+ specification file is a relative path.
|
||||||
(cmd (concat
|
(cmd (concat
|
||||||
tla+-java-path " -cp " tla+-tlatools-path
|
tla+-java-path " -cp " tla+-tlatools-path
|
||||||
" tlc2.TLC "
|
" tlc2.TLC "
|
||||||
|
tla+-tlc-deadlock " "
|
||||||
|
tla+-tlc-simulate " "
|
||||||
|
tla+-tlc-depth " "
|
||||||
|
tla+-tlc-coverage " "
|
||||||
|
tla+-tlc-workers " "
|
||||||
" -config " cfgfile " "
|
" -config " cfgfile " "
|
||||||
finame))
|
finame))
|
||||||
(output (shell-command-to-string cmd)))
|
(output (shell-command-to-string cmd)))
|
||||||
|
@ -513,8 +552,10 @@ 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)
|
||||||
|
(tla+/find-error-marks)
|
||||||
(other-window 1)
|
(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))
|
(let* ((filename (buffer-file-name))
|
||||||
(oldfile (replace-regexp-in-string
|
(oldfile (replace-regexp-in-string
|
||||||
".tla$" ".old" filename))
|
".tla$" ".old" filename))
|
||||||
(pcalbuf (get-buffer-create "*pcal.trans*"))
|
(pcalbuf (get-buffer-create
|
||||||
|
(format "*pcal.trans* [%s]" (buffer-name))))
|
||||||
(cmd (concat
|
(cmd (concat
|
||||||
tla+-java-path " -cp " tla+-tlatools-path
|
tla+-java-path " -cp " tla+-tlatools-path
|
||||||
" pcal.trans "filename ))
|
" pcal.trans "filename ))
|
||||||
|
@ -696,6 +738,11 @@ Steps done by this function:
|
||||||
5. goto line and column.
|
5. goto line and column.
|
||||||
"
|
"
|
||||||
(let* ((pos (point))
|
(let* ((pos (point))
|
||||||
|
(buffername
|
||||||
|
(replace-regexp-in-string
|
||||||
|
"\\*.*\\* \\[\\(.*\\)\\]"
|
||||||
|
"\\1"
|
||||||
|
(buffer-name)))
|
||||||
(the-button (button-at pos))
|
(the-button (button-at pos))
|
||||||
(text (button-label the-button))
|
(text (button-label the-button))
|
||||||
(s (string-match
|
(s (string-match
|
||||||
|
@ -708,15 +755,10 @@ Steps done by this function:
|
||||||
(col (string-to-number (match-string 3 text))))
|
(col (string-to-number (match-string 3 text))))
|
||||||
;(message (format "Button pressed: %s" text))
|
;(message (format "Button pressed: %s" text))
|
||||||
(progn
|
(progn
|
||||||
;(switch-to-buffer (other-buffer))
|
(switch-to-buffer-other-window buffername)
|
||||||
(other-window 1)
|
|
||||||
;(switch-to-buffer (other-buffer))
|
|
||||||
;(switch-to-buffer-other-window (current-buffer))
|
|
||||||
(goto-char (point-min))
|
(goto-char (point-min))
|
||||||
(goto-line line)
|
(goto-line line)
|
||||||
(forward-char col)
|
(forward-char (- col 1))
|
||||||
;(switch-to-buffer (other-buffer))
|
|
||||||
;(message "%s" (buffer-name))
|
|
||||||
)))
|
)))
|
||||||
|
|
||||||
(defun tla+/make-link-button (begin end)
|
(defun tla+/make-link-button (begin end)
|
||||||
|
@ -756,7 +798,7 @@ The procedure works by:
|
||||||
(colnum (match-beginning 3))
|
(colnum (match-beginning 3))
|
||||||
(rend (+ colnum (- (length (int-to-string colnum)) 0)))
|
(rend (+ colnum (- (length (int-to-string colnum)) 0)))
|
||||||
)
|
)
|
||||||
;(message "%s %s" linenum colnum)
|
(message "%s %s" linenum colnum)
|
||||||
;(message "%d %d" rstart rend)
|
;(message "%d %d" rstart rend)
|
||||||
(tla+/make-link-button rstart rend)
|
(tla+/make-link-button rstart rend)
|
||||||
))))
|
))))
|
||||||
|
|
Loading…
Reference in New Issue