Might be useful to be able to generate pdf from command line

[dgpv]

With a command like this:

java -cp ${TLATOOLSDIR}/tla2tools.jar tla2tex.TLA \
	    -metadir metadir \
	    -latexOutputExt pdf \
	    -latexCommand pdflatex \
	    -ptSize 12 \
	    -shade \
	    SomeFile.tla