diff --git a/ChangeLog b/ChangeLog index 6a96db8..d015231 100644 --- a/ChangeLog +++ b/ChangeLog @@ -1,3 +1,35 @@ +2020-08-27 Christian Barthel + + * 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 + + * 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.. 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 * lisp/tla+-mode.el (tla+-tlc-depth): tune depth diff --git a/lisp/tla+-mode.el b/lisp/tla+-mode.el index 08577c5..1592232 100644 --- a/lisp/tla+-mode.el +++ b/lisp/tla+-mode.el @@ -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))