Line Numbers with tla2tex.TeX

[Willy Schultz]

Is there a way to include line numbers in the output of tla2tex.TeX? This comment seems to indicate it may have been disabled for some reason. I tried the -number option but the tool did not recognize it.

[Christian Barthel]

Willy Schultz <will...@gmail.com> writes:

> Is there a way to include line numbers in the output of tla2tex.TeX? This
> comment

> <https://github.com/tlaplus/tlaplus/blob/1477e11becd86d971aad4ddef2a3ef23afcc495c/tlatools/org.lamport.tlatools/src/tla2tex/TeX.java#L518-L524>

> seems to indicate it may have been disabled for some reason. I tried the
> -number option but the tool did not recognize it.

I can not comment on the source code change but I am using the
command above to generate a .tex and .ps file:

java -cp ../tla2tools/tla2tools_1.8.0.jar tla2tex.TLA \
-shade -number file.tla

This generates line numbers and I am then using the .tex file for
further processing.

If you prefer using tla2tex.TeX: I also tested embedding the TLA+
specification within a `linenumbers' (LaTeX package: lineno)
block and this generates linenumbers as well:

--8<---------------cut here---------------start------------->8---
\documentclass{article}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{tlatex}
\usepackage{color}
\definecolor{boxshade}{gray}{.85}
\setboolean{shading}{true}
\usepackage{lineno} %%% use lineno package to generate line numbers
\nolinenumbers %%% by default, turn line numbering off.

\begin{document}
Some explanation on \texttt{GCD}:

\begin{linenumbers}
\begin{tla}
-------------------------------- MODULE GCD --------------------------------
EXTENDS Integers
----------------------------------------------------------------------------
Divides(p, n) == \E q \in Int : n = q * p
DivisorsOf(n) == {p \in Int : Divides(p, n)}

SetMax(S) == CHOOSE i \in S : \A j \in S : i >= j

GCD(m, n) == SetMax(DivisorsOf(m) \cap DivisorsOf(n)) \* gcd of $m$ and $n$
SetGCD(T) == SetMax({d \in Int : \A t \in T : Divides(d, t)})
=============================================================================
\end{tla}
\end{linenumbers}

Followup text without line numbering.
\end{document}
--8<---------------cut here---------------end--------------->8---

Commands to generate a PDF file:

java -cp tla+/tla2tools/tla2tools_1.8.0.jar tla2tex.TeX doc.tex
pdflatex doc.tex

Hope that helps,
Christian

--
Christian Barthel <b...@online.de>