[tlaplus] Re: Get the raw LaTeX from the spec instead of an exported PDF?

["thomas...@xxxxxxxxx" <thomasgebert@xxxxxxxxx>]

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. 

On Tuesday, August 25, 2020 at 1:12:57 PM UTC-4 will...@xxxxxxxxx wrote:

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.

On Tuesday, August 25, 2020 at 12:06:27 PM UTC-4 thomas...@xxxxxxxxx wrote:

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? 

-- 
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/7a66210b-d90d-4d2a-95ae-a8768b398c2an%40googlegroups.com.