add PlusCal transation

pcal.trans translates PlusCal comments to a
TLA+ specification.  This commits adds a
function to execute the translator.
Christian Barthel 2020-01-05 10:46:54 +01:00
parent 279db98723
commit 1a13c39218
1 changed files with 48 additions and 3 deletions

View File

@ -58,7 +58,7 @@
:group 'tla+)
(defcustom tla+-tlatools-path
"Path to the TLA+ `tlatools.jar' file"
:type 'file
:group 'tla+)
@ -97,6 +97,7 @@
(define-key map (kbd "C-c C-t e") 'tla+-run-tlatex-dvi)
(define-key map (kbd "C-c C-t o") 'tla+-open-dvi)
(define-key map (kbd "C-c C-t c") 'tla+-run-sany)
(define-key map (kbd "C-c C-t p") 'tla+-run-pluscal)
;; Main TLA+ Menu:
(bindings--define-key map [menu-bar tla+]
@ -257,7 +258,7 @@
;; Operators
(bindings--define-key menu-map [operator]
(cons "Insert Operator.." operator-map))
(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
;; Action Operators
(bindings--define-key operator-map [action-operator]
(cons "Action Operator" action-operator-map))
@ -344,6 +345,12 @@
;; Main Menu
(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
(bindings--define-key map [menu-bar tla+ tla+-run-pluscal]
'(menu-item "Run PlusCal Translator" tla+-run-pluscal
"Run pcal.trans"
"(Translator from PlusCal algorithm language to TLA+)"))
(bindings--define-key map [menu-bar tla+ tla+-run-sany]
'(menu-item "Run Syntax Checker" tla+-run-sany
@ -353,7 +360,7 @@
(bindings--define-key map [menu-bar tla+ tla+-create-module]
'(menu-item "Create new Module" tla+-create-module
:help "Create a new TLA+ Module"))
(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
;(bindings--define-key map [menu-bar tla+ sep] menu-bar-separator)
"Keymap for `tla+-mode'.")
@ -412,6 +419,8 @@ The function executes the TLA+ Syntax checker and reports errors
in a new frame. Errors are clickable buttons and the user can
directly go to the error line.
It is meant to be run from a TLA+ Specification buffer.
1. execute the tla2sany.SANY program
2. the output of the shell-command is inserted into a newly
@ -435,6 +444,42 @@ Operation:
(insert output)
(defun tla+-run-pluscal ()
"This function runs pcal.trans (PlusCal Translator to TLA+)
This function executes the PlusCal Translator on the current
buffer (Assumption: the buffer is a TLA+ buffer that contains
PlusCal code).
On success, the buffer will be reloaded and a message will be
printed. On failure (i.e. the exit code of the shell command
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*"))
(cmd (concat
tla+-java-path " -cp " tla+-tlatools-path
" pcal.trans "filename ))
(output (shell-command cmd)))
(if (= output 0)
(revert-buffer nil t)
(message (concat
"Successfully Transalted"
" - You can visit the old file at "
(other-window 1)
(switch-to-buffer pcalbuf)
(shell-command-to-string cmd))
(message "Translation Failed")))))
(defun tla+-open-dvi (buffername)
"Function to open a DVI file.
This function starts the `xdvi' utility and opens the TLA+