On Tuesday, August 25, 2020 at 4:29:54 PM UTC-4 thomas...@xxxxxxxxx wrote:
That works, I was able to grab it from the `.toolbox` folder.
I can't imagine it would be too hard to add this as an official feature for the toolbox, would it? It has to produce the TeX anyway to create the PDF, I would think it would be pretty straightforward to add an option to have a little menu-item underneath saying "export TeX" or something.
I'm not sure if there's an officially supported way to get the TeX source directly from inside the Toolbox, but if you click "File > Produce PDF Version", the TeX output from the PDF generation should be placed in the *.toolbox directory of your spec. For example, if your module is named "Spec", you should find a .tex file at "Spec.toolbox/Spec.tex". You could retrieve it manually from that location. If you want to bypass the Toolbox entirely, you can generate the TeX source from the command line using the `java tla2tex.TLA` tool directly.
Hello! I have a spec that I designed in the Toolbox, and I want to take the spec and include it into a paper I'm writing. Is there a way to export the raw LaTeX code from the toolbox instead of just the PDF?