[tlaplus] Running tla2tex.TeX on a TeX file without document preamble

[Christian Barthel <bch@xxxxxxxxx>]

Hello,

I'd like to include TLA+ source code listings in a LaTeX TeX
file.  The file is structured with various "\input{document}"
commands.

Is it possible to run tla2tex.TeX on "document.tex" (the tex file
has no \begin{document} preamble..) to generate the TLA+ pretty
printed tex code?

When doing so, I get an error:


$ java -cp tla2tools.jar tla2tex.TeX  document.tex
tla2tex.TeX Version 1.0 created 12 Apr 2013 
No file ch6-fb1.log

TLATeX unrecoverable error:

 -- Input file has no \begin{document}.

Exception in thread "main" tla2tex.TLA2TexException:
    TLATeX unrecoverable error:
        at tla2tex.Debug.ReportError(Debug.java:26)
        at tla2tex.TeX.main(TeX.java:192)


-- 
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/87pn7cbkr3.fsf%40barthel.ch.