Running tla2tex.TeX on a TeX file without document preamble

[Christian Barthel]

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 <b...@online.de>