Email Gateway (Aug 22 2022 at 15:38): Email Gateway (Aug 22 2022 at 15:38):From: Burkhart Wolff <Burkhart.Wolff@lri.fr>
Dear all,
I’m trying to define a new command which
should be mapped to an own LaTeX markup during documentation.
I tried to understand the Isabelle code for “text” or “section”
but could not figure out where exactly this is mapped to
\isamarkupsection instead of \isacommand … ?
More generally speaking, is there somewhere a more synthetic
description on the LaTeX engine ? (In the reference manual, I did not
find s th which goes beyond certain options and some LaTeX tricks …
The referenced paper on the Pretty.T structure is a bit far away ...)
Trans in advance,
B. Wolff
Email Gateway (Aug 22 2022 at 15:38):From: Makarius <makarius@sketis.net>
On 23/06/17 15:32, Burkhart Wolff wrote:
I’m trying to define a new command which
should be mapped to an own LaTeX markup during documentation.I tried to understand the Isabelle code for “text” or “section”
but could not figure out where exactly this is mapped to
\isamarkupsection instead of \isacommand … ?
I am unsure if defining a new document markup command will actually
work. It started out as a super-generic mechanism many years ago, but in
recent years a fixed canon of commands has emerged: chapter, section,
subsection, text etc.
There are other ways to modify the meaning of the existing markup
commands using document tags. For example, see
$ISABELLE_HOME/src/Doc/Implementation for occurrences of "text %mlref"
of "text %mlex". The LaTeX macros are defined here:
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Doc/Implementation/document/style.sty#l30
It should possible to play arbitrary LaTeX tricks via such tag environments.
More generally speaking, is there somewhere a more synthetic
description on the LaTeX engine ? (In the reference manual, I did not
find s th which goes beyond certain options and some LaTeX tricks …
The referenced paper on the Pretty.T structure is a bit far away ...)
Pretty.T is only relevant for output, e.g. of @{term}.
The main typesetting happens in
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2016-1/src/Pure/Thy/thy_output.ML
but that is about to change -- it might happen next week or next year,
or later.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC