Re: [tlaplus] tlatex fragments and beamer presentations

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

On 01.08.19 09:13, 'Marko Schuetz-Schmuck' via tlaplus wrote:
> Dear All,
> 
> I'm preparing some beamer slides to summarize some of Leslies video
> lectures and it seems there is a conflict between tlatex and
> beamer. Apparently \. is defined in both and running latex on the
> resulting file will end with
> 
> Runaway argument?
> ! File ended while scanning use of \next.
> 
> I intend to use prepare more beamer slides that will involve TLA+ and
> would welcome advice on how others deal with this combination.
> 
> Here is a simplified example
> 
> \documentclass[compress,notes=hide]{beamer}
> \let\oldImplies=\implies
> \let\implies=\undefined
> \usepackage{tlatex}
> \begin{document}
> 
> \begin{frame}{Slide title}
> \begin{tla}
> IF pc = "start" THEN 
>    i' \in 0..1000 /\
>    pc' = "middle"
> ELSE IF pc = "middle" THEN
>    i' = i + 1 /\
>    pc' = "done"
> ELSE FALSE
> \end{tla}
> \begin{tlatex}
> \@x{ {\IF} pc \.{=}\@w{start} \.{\THEN}}%
> \@x{\@s{13.31} i \.{'}\@s{5.25} \.{\in} 0 \.{\dotdot} 1000 \.{\land}}%
> \@x{\@s{13.31} pc \.{'} \.{=}\@w{middle}}%
> \@x{ \.{\ELSE} {\IF} pc \.{=}\@w{middle} \.{\THEN}}%
> \@x{\@s{12.29} i \.{'} \.{=} i \.{+} 1 \.{\land}}%
> \@x{\@s{12.29} pc \.{'} \.{=}\@w{done}}%
> \@x{ \.{\ELSE} {\FALSE}}%
> \end{tlatex}
> \end{frame}
> \end{document}
> 
> 
> Best regards,
> 
> Marko
> 

Hi Marko,

I frequently embed TLA+ and PlusCal in Beamer presentations.  Although I
use LyX [1] as a front-end to LaTex, my setup [2] might be useful for
you.  See the lyx, latex, and pdf files [3] as a proof of concept for
your if-then-else above.

Hope this helps,
Markus

[1] https://www.lyx.org/
[2] https://lemmster.de/tla-in-lyx.html
[3] https://tla.msr-inria.inria.fr/kuppe/poc.zip


-- 
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/e01b34b3-7b14-3ba2-a3bd-b7aa11f0da8e%40lemmster.de.