Commit Graph

9 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
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