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

remove default paths, add error checks when toolbox missing 

* lisp/tla+-mode.el (tla+-java-path):
(tla+-dot-binary):
remove some default paths that may be not useful or
helpful for other users.
(tla+-run-sany):
(tla+-run-model):
(tla+-run-pluscal):
(tla+-run-tlatex):
(tla+-run-model): add an error check (if the
tla+-tlatools-path is not set, print an error message)
(tla+-run-dot): run dot only when the binary to dot
is given.
This commit is contained in:
Christian Barthel 2020-08-27 17:16:13 +02:00
parent 6d84767a52
commit 8e2341f849
2 changed files with 49 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

32
ChangeLog
View File

@ -1,3 +1,35 @@
2020-08-27 Christian Barthel <bch@online.de>
* lisp/tla+-mode.el (tla+-java-path):
(tla+-dot-binary):
remove some default paths that may be not useful or
helpful for other users.
(tla+-run-sany):
(tla+-run-model):
(tla+-run-pluscal):
(tla+-run-tlatex):
(tla+-run-model): add an error check (if the
tla+-tlatools-path is not set, print an error message)
(tla+-run-dot): run dot only when the binary to dot
is given.
2020-08-03 Christian Barthel <bch@online.de>
* org/Test.org: add an example org file.
this shows the usage of org-babel-tangle in
combination with TLA+ (it may be used to
further comment on TLA+ specifications).
* lisp/tla+-mode.el: update URLs, remove
unnecessary comments, cleanup whitespace and
wrap lines.
(tlc-widget-example): if a TLC cfg already
exists, copy it to .old.<seconds>. erase
the buffer then and insert the new TLC
config into the buffer.
Add the current time to the tlc config.
2020-08-02 Christian Barthel <bch@online.de>
* lisp/tla+-mode.el (tla+-tlc-depth): tune depth

23
lisp/tla+-mode.el
View File

@ -51,7 +51,7 @@
:group 'tla+)
(defcustom tla+-tlatools-path
"/usr/home/bch/tmp/tlaplus/tlatools/dist/tla2tools_1.6.0.jar"
nil
"Path to the TLA+ `tlatools.jar' toolbox java archive"
:type 'file
:group 'tla+)
@ -117,7 +117,7 @@
:type 'string)
(defcustom tla+-dot-binary
"dot"
nil
"path to dot binary"
:type 'string)
@ -562,6 +562,8 @@ Operation:
3. errors are converted into clickable buttons by using the
`tla+/find-error-marks' function."
(interactive)
(if (not tla+-tlatools-path)
(error "need the TLA+ toolbox java archive: tla+-tlatools-path"))
(let* ((filename (buffer-file-name))
(sanybuffer
(get-buffer-create
@ -582,10 +584,11 @@ Operation:
(other-window 1))))
(defun tla+-run-dot ()
(let ((cmd (format "%s -Tpng states.dot > %s"
tla+-dot-binary
tla+-dot-convert)))
(shell-command-to-string cmd)))
(if tla+-dot-binary
(let ((cmd (format "%s -Tpng states.dot > %s"
tla+-dot-binary
tla+-dot-convert)))
(shell-command-to-string cmd))))
(defun tla+-run-model (cfgfile)
"Run the tlc2.TLC Model checker
@ -605,6 +608,8 @@ Note: The TLA+ specification file is a relative path.
(concat
(file-name-base (buffer-file-name))
".cfg" ))))
(if (not tla+-tlatools-path)
(error "need the TLA+ toolbox java archive: tla+-tlatools-path"))
(let* ((filename (buffer-file-name))
(tlcbufname (format "*tlc2.TLC* [%s]" (buffer-name)))
;(tlcbuffer (get-buffer-create
@ -682,6 +687,9 @@ was not 0), an error message will be printed.
tla+-java-path " -cp " tla+-tlatools-path
" pcal.trans "filename ))
(output (shell-command cmd)))
(if (not tla+-tlatools-path)
(error
"need the TLA+ toolbox java archive: tla+-tlatools-path"))
(if (= output 0)
(progn
(revert-buffer nil t)
@ -783,6 +791,9 @@ The function executes one or two shell commands synchronously."
(convert2ps (concat
tla+-dvips-path " " dvipath)))
(progn
(if (not tla+-tlatools-path)
(error
"need the TLA+ toolbox java archive: tla+-tlatools-path"))
(cond
((eq type 'pdf)
(shell-command convert2pdf))