Commit Graph

24 Commits (master)

Author SHA1 Message Date
Christian Barthel bf13ea44db Add a few tla symbols and load them to prettify them on command
- define some TLA+ symbols
- Use `M-x prettify-symbols-mode' to view them.
2021-04-13 19:44:49 +02:00
Christian Barthel 09941c5311 Add TLA+ Repl Shell elisp wrapper
- add a function to start a REPL TLA+ shell
- add menu button to launch repl shell
2021-02-19 21:42:36 +01:00
Christian Barthel 71b6abbf9d Fix whitespace, add execution cmd message
- fixup whitespace globally
- dump executed command in notification area
2021-02-19 21:18:08 +01:00
bch 78a196b94d example image 2020-08-27 18:50:59 +00:00
bch 2d679612c1 README
2020-08-27 18:49:21 +00:00
Christian Barthel 9dc03f8cbc example pic 2020-08-27 20:42:27 +02:00
Christian Barthel 8e2341f849 remove default paths, add error checks when toolbox missing
* lisp/tla+-mode.el (tla+-java-path):
remove some default paths that may be not useful or
helpful for other users.
(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-27 17:16:13 +02:00
Christian Barthel 6d84767a52 handling of TLC config files
* 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.<seconds>.  erase
  the buffer then and insert the new TLC
  config into the buffer.
  Add the current time to the tlc config.

  * 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).
2020-08-03 05:11:09 +02:00
Christian Barthel 6ba78769a5 tlc window handling improvement, dot(1) usage
* lisp/tla+-mode.el (tla+-tlc-depth): tune depth
  parameter, default to 1000 now.
  (tla+-tlc-workers): tune worker threads (at least
  2 threads should be used by default)
  (tla+-dot-convert, tla+-dot-binary): dot(1)
  customization variables.
  (tla+-run-dot): elisp function to run dot(1) and
  convert the state graph to a PNG file
  (tla+-run-model): automatically generate the PNG
  output file, change  the window handling.  It
  seems better to only show the tlc buffer output
  once (when it is a newly created buffer).  The
  user may kill it, or arrange it in such a way
  that the output can be read by another tlc model
  check run.  Also: set the bufffer to readonly.
  (tlc-widget-example): remove the cfgname; seems
  that the lambda expressions do not see the cfgname
  anyway so I have to reconstruct it.
* ChangeLog: add a changelog file
2020-08-02 22:28:31 +02:00
Christian Barthel b84b64612a select and use tlc parameters
- move documentation to the `describe-mode' section
- implement TLC command line options: for each TLC
  config file, there might be a .cfgtlcopt file that
  contains an association list for controlling the
  parameters when running the TLC model checker.
  - add tla+/read-options, tla+/write-options and
    tla+/add-option to manipulate the option
  - extend the widget to allow selecting various
- use the TLA+ mode for the .cfg file as well; insert
  a local variable block for selecting the appropriate
  emacs mode.
2020-07-19 10:05:13 +02:00
Christian Barthel deba3792c9 update log info option, syntax highlighting
- add new Update ChangeLog function
- do not highlight keywords inside comments
- use fundamental-mode as basis
- dump the dot state by default
2020-07-18 21:54:02 +02:00
Christian Barthel a8ebeb008c moving source code file into subdirectory 2020-02-20 10:47:16 +01:00
Christian Barthel 5f04536a35 tlc settings, tlc error buttons
- 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
2020-02-18 22:12:12 +01:00
Christian Barthel 1522267517 work on TLC config dialogue
this commit adds a small graphical interface
to create models which can be executed by the
TLC model checker.
2020-02-15 20:02:07 +01:00
Christian Barthel a29978acaf references, go back to "original window"
this commit adds some references to get the
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.
2020-01-06 22:13:51 +01:00
Christian Barthel 30d6a1b7ee add model checker run function
add a new function to run the tla+ model
checker on a model.
2020-01-05 14:11:19 +01:00
Christian Barthel 1a13c39218 add PlusCal transation
pcal.trans translates PlusCal comments to a
TLA+ specification.  This commits adds a
function to execute the translator.
2020-01-05 10:46:54 +01:00
Christian Barthel 279db98723 features and installation instructions
short explanation about the features of the
tla+-mode and how to install it.
2020-01-05 09:47:32 +01:00
Christian Barthel 4b57968fa3 new keyword LET/IN
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
2020-01-04 09:55:55 +01:00
Christian Barthel 9d6c2da190 additional keyword, regex fix 2019-12-28 21:25:12 +01:00
Christian Barthel c58bbb6671 comments, modul operators, mark error messages
- add comments
- add keybord shortcuts
- add modul operators (from naturals, sequences)
- add functions to mark error messages in the SANY
  check buffer.
2019-12-26 08:16:03 +01:00
Christian Barthel 87707476af add operator insertion menu, ps/pdf conversion, etc.
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)
- add action and temporal operators (i.e. functions to insert
  those symbols).  the help text is the one found on the tla+
- more syntax highlighting for more constants and types
2019-12-23 16:50:36 +01:00
Christian Barthel 84d7eafeea more keywords, the tla+-open-dvi function
this commit adds a few more keywords that should be highligted and
adds a new function to open the dvi file.
2019-12-22 22:36:00 +01:00
Christian Barthel 2e6a2c6a09 first defintions for a new TLA+ mode
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
2019-12-19 23:39:50 +01:00