Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Items displayed in Sidekick


view this post on Zulip Email Gateway (Nov 12 2022 at 13:01):

From: Peter Lammich <lammich@in.tum.de>
Hello List,

what determines if an item is displayed in the sidekick panel? As far as
I can see, this is currently hardcoded in Pure/Isar/Keyword.scala, used
by the parsers in document_structure.scala.

Is there any way to get my own command displayed in sidekick, without
modifying and recompiling Isabelle distribution code?

Best,

Peter

view this post on Zulip Email Gateway (Nov 12 2022 at 13:13):

From: Peter Lammich <lammich@in.tum.de>
Clarification:

I want to define a command "frame", that generates a latex beamer frame.

I understand it should be one of the document_xxx kinds (document_raw or
so). However, these are not displayed in Sidekick.

And the sectioning commands to be displayed in Sidekick are hardcoded in
Pure/Thy/thy_header.scala.

view this post on Zulip Email Gateway (Nov 13 2022 at 17:38):

From: Makarius <makarius@sketis.net>
It is better to re-use existing section commands like 'chapter' or 'section',
and merely adjust the LaTeX output.

Just after the Isabelle2022 release, I have made a demo for good old FoilTeX
here:
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/Doc/Demo_FoilTeX/;8dbda1b611e9

I want to do Beamer as well, but have never used it so far.

So maybe you just show me your usual Beamer LaTeX setup, so that I can learn
from it. Everybody else is invited to send their favourite Beamer tweaks, too.

Makarius


Last updated: Apr 19 2024 at 04:17 UTC