hengxin / tla2tex

TLA+ Code to TeX Code using tla2tools.jar

tla2tex

TLA+ code to TeX code

How to do that?

• Put your tla code in between \begin{tla} and \end{tla} in file like tla2tex-example-tla.tex.
  • Ignore the code in between \begin{\tlatex} and \end{\tlatex} now.
• Run java -cp tla2tools.jar tla2tex.TeX tlatex-example-tla.tex
  • This will automatically generate that code in between \begin{\tlatex} and \end{\tlatex}.
  • Important Note: You'd better run java -cp under the directory of tlatex-example-tla.tex. Otherwise, you may get a renaming error and information indicating that some .new file was generated in a different directory.
  • -cp tla2tools.jar: make sure that tla2tools.jar is in your path; use your-path-to-tla2tools.jar when necessary.
• Compile tlatex-example-tla.tex to produce the pdf version which can be inserted into your LaTeX document as usual.
  • Make sure that tlatex.sty is in your path.

For detailed info, see tla2tex-readme.md.

tla2tex's Issues

Show/Hide line numbers in generated pdfs

• Show/Hide line no.
• Allow to specify the starting line no. for code snippets

TODO list for tla2tex tools

• Line space

  • Especially, above/below "======="

• Smaller fonts

• Keywords highlight

• longer "========"

• Show/Hidden Line No

• Automation:

  • Changes detect
  • Copy and rename
  • Delete "preamble"