TLA+ major mode for Emacs

[Christian Barthel]

Hello,

I am currently in the process of learning TLA+ and how to specify
software. To do that, I created a Major-Mode to edit TLA+
specifications within the Emacs ecosystem(*). If someone is also
interested in writing specifications with Emacs, the elisp code
can be downloaded here [1].

This is one of my first emacs major-modes. Any hints, tips or
further additions are welcome. The implemented functionality:

- Syntax Highlighting for TLA+ Specification Files
- Running `SANY Syntactic Analyzer' on TLA+ files,
default keybinding: `C-c C-t c'.
- Exporting TLA+ Specification files with TLATeX to
DVI, PS or PDF files (Export it with `C-c C-t e'
and open the viewer `C-c C-t o')
- Inserting TLA+ Operators with an easy to use menu
or typical Emacs keystrokes.
- Use templates to generate Modules
- An Emacs widget to create TLC configuration files
- Options to run the TLC model checker on TLA+
specifications (`C-c C-t m').
- Translate PlusCal code to TLA+ specification
with `C-c C-t p'.

To install and configure:
(load </path/to/tla+-mode.el>)
(require 'tla+-mode)
(setq tla+-tlatools-path </path/to/tla2tools.jar>)
See more details with `describe-mode'.

I will try to further extend the elisp code while I am reading
the `Specifying Systems' book. The current version seems to
support most of what I am currently using: write a spec, do some
syntax highlighting, check the spec (c-c c-t c), run the TLaTeX
pretty printer (c-c c-t e) or try to model check with TLC
(c-c c-t m).

Any additional improvements are welcome,
Christian


(*) I am using BSD operating systems and it seems that the
eclipse TLA+ Toolbox is not running on that operating system.
However, the tla2tools.jar can be used with a Java runtime.

[1] Emacs tla+-mode.el:
https://git.sdf.org/bch/tlamode/
Raw file:
https://git.sdf.org/bch/tlamode/raw/branch/master/lisp/tla+-mode.el