[tlaplus] TLA+ major mode for Emacs

[Christian Barthel <bch@xxxxxxxxx>]

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

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87sgc83xn4.fsf%40barthel.ch.