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

[Willy Schultz <will62794@xxxxxxxxx>]

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/8a02c3c7-32ef-4f61-947d-56874b073c32n%40googlegroups.com.