Re: [tlaplus] Line Numbers with tla2tex.TeX

[Christian Barthel <bch@xxxxxxxxx>]

Willy Schultz <will62794@xxxxxxxxx> 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 <bch@xxxxxxxxx>

-- 
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/87lfb2owu6.fsf%40x230a3.onfire.org.