- compilation output buffers (sany, tlc) store
the name of the TLA+ file.
this can be used to jump back to the buffer
if the tla+/find-error-marks highlights
"line:column" markers.
- use tla+/find-error-marks with the TLC output
- add additional tlc global setting
this commit adds some references to get the
tlatoolbox.jar.
i also changed the behavior of running sany
and tlc slightly: if a new window pops up,
i switch back to the tla buffer. a simple
c-x 1 gets rid of the message buffer.
this commit adds the new keyword
LET..IN as seen in chapter 5. Aditionally, the
tla+-run-tlatex-dvi comment has been clarified
i.e. an explanation for the argument was added
- add comments
- add keybord shortcuts
- add modul operators (from naturals, sequences)
- add functions to mark error messages in the SANY
check buffer.
this commit adds
- more comments,
- change the path to simple binary name. with that, the
$PATH variable may be used. Hard coding the path is
unnecessarily restrictive.
- add dvips and dvipdf convertion (two additional customization
parameters define the path to the dvipdf(1) and dvips(1)
programs
- add action and temporal operators (i.e. functions to insert
those symbols). the help text is the one found on the tla+
cheatsheet.
- more syntax highlighting for more constants and types
goal is to implement a convenient mode to read and write
TLA+ specifications. This commit adds the first few
functions to
- create a new module
- run SANY on a TLA+ module
- run TLaTeX export and create DVI file format
- some bascic font-highlighting
- comments can be created
