Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] beamer, once again

Email Gateway (Aug 23 2022 at 09:14):

From: Walther Neuper <walther.neuper@jku.at>
I run into the problem with combining

\documentclass{beamer}
\usepackage{isabelle,isabellesym}

already addressed in

https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-October/msg00005.html

I follow the hints given there,

* delete {hyperref} from "pdfsetup.sty"
* rename "pdfsetup.sty" to "pdfsetupbeamer.sty"
* include "pdfsetupbeamer.sty" in "ROOT" within "document_files (in "output/document")"

but then get the error

isabelle document -d output/document -o pdf -n document
*** Latex error (line 42 of "/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document/root.tex"):
*** File ended while scanning use of \@fileswith@ptions.
*** <inserted text>
*** \par

I also notice, that "isabelle build" restores "pdfsetup.sty" in "output/document".

Is there somebody who can give me a hint such that I need not dig into tex intricacies
(I see: replacing "{hyperref}" by "{}" shifts the error to a later location),
or need not understand details of "isabelle build"
(achieving "pdfsetupbeamer.sty" actually to replace "pdfsetup.sty")?

Any help is appreciated,
Walther
pdfsetupbeamer.sty

Email Gateway (Aug 23 2022 at 09:14):

From: Walther Neuper <walther.neuper@jku.at>
sorry, there was an error in my pdfsetupbeamer.sty, correction attached.

Now the error shifts to the first \input{..} in root.tex:

theory "slides-isabisac.Slides_Content"

0.046s elapsed time, 0.072s cpu time, 0.040s GC time

isabelle document -d output/document -o pdf -n document
*** Latex error (line 75 of "/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document/root.tex"):
*** File ended while scanning use of \beamer@collect@@body.
*** <inserted text>
*** \par
*** \input{Slides_Content.tex}
*** Latex error (line 84 of "/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document/root.tex"):
*** \begin{frame} on input line 35 ended by \end{docume
*** nt}.

*** ...

*** \end{document}
*** Failed to build document in "/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document"
Unfinished session(s): slides-isabisac

Is there someone who has a clue without further effort?

Walther
pdfsetupbeamer.sty

Email Gateway (Aug 23 2022 at 09:14):

From: Walther Neuper <walther.neuper@jku.at>
On 18.06.20 13:20, John F. Hughes wrote:

If I remember correctly, when I "input" foo.tex in my LaTeX files, I
typically type

\input{foo}

i.e., the .tex gets "assumed". But I have no idea whether this will be
of any help. Best of luck. The whole document-prep aspect of Isabelle
still seems like dark magic to me. :(

Thank you for comments!

The "\input{foo.tex}" in the examples seems trying to clarify, that some
dedicated "Foo.thy" first are translated into "Foo.tex" by "isabelle
build" and the latter are used by LaTeX.

But still no clue about \documentclass{beamer} +
\usepackage{isabelle,isabellesym}.

Among Isabelle users much learning happens by "looking over the
shoulder" of colleagues, in particular with elementary technicalities
like slides creation; so I understand why I'm waiting for support.

On Thu, Jun 18, 2020 at 4:14 AM Walther Neuper <walther.neuper@jku.at
<mailto:walther.neuper@jku.at>> wrote:

On 16.06.20 21:58, Walther Neuper wrote:
> I run into the problem with combining
>
>    \documentclass{beamer}
>    \usepackage{isabelle,isabellesym}
>
> already addressed in
>
>   
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2015-October/msg00005.html
>
> I follow the hints given there,

sorry, there was an error in my pdfsetupbeamer.sty, correction
attached.

Now the error shifts to the first \input{..} in root.tex:

### theory "slides-isabisac.Slides_Content"
### 0.046s elapsed time, 0.072s cpu time, 0.040s GC time
isabelle document -d output/document -o pdf -n document
*** Latex error (line 75 of
"/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document/root.tex"):
***   File ended while scanning use of \beamer@collect@@body.
***   <inserted text>
***                   \par
***   \input{Slides_Content.tex}
*** Latex error (line 84 of
"/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document/root.tex"):
***   \begin{frame} on input line 35 ended by \end{docume
***   nt}.
***   
***    ...                                             
***                                                     
***   \end{document}
*** Failed to build document in
"/home/wneuper/material/texts/emat/lucin-isa/p-slides-isabisac/output/document"
Unfinished session(s): slides-isabisac

Is there someone who has a clue without further effort?

Walther

Last updated: Nov 21 2024 at 12:39 UTC