Email Gateway (Aug 18 2022 at 13:01): Email Gateway (Aug 18 2022 at 13:01):From: Christian Doczkal <c.doczkal@stud.uni-saarland.de>
Hello
I'm trying to specify additional tags for the isabelle document
preparation. Simply adding the tags to isatool usedir via -V "/foo" does
not allow folding of commands.
isabelle.sty checks for isabelletags.sty but this should probably be
generic to different versions (document and outline) so how do I get new
tags into the machinery?
smime.p7s
Email Gateway (Aug 18 2022 at 13:04):From: Makarius <makarius@sketis.net>
On Thu, 19 Feb 2009, Christian Doczkal wrote:
I'm trying to specify additional tags for the isabelle document
preparation. Simply adding the tags to isatool usedir via -V "/foo" does
not allow folding of commands.
Well, it should work. As explained in the system manual (cf. "usedir"
tool), option -V allows to specify named document "versions" with certain
meaning of tags in a high-level way. The example -V "/foo" is
syntactically incorrect. What exactly did you try here?
isabelle.sty checks for isabelletags.sty but this should probably be
generic to different versions (document and outline) so how do I get new
tags into the machinery?
Seen from the bottom end, tags are introduced by using them in the text,
via %mytag, and defining suitable LaTeX macros \isadelimmytag, \isamytag
etc. (this can be done in root.tex, for example). A convenient way works
via the meta-macros \isakeeptag, \isadroptag, \isafoldtag from
isabelle.sty, e.g. like this:
\isafoldtag{mytag}
You can also start with \isakeeptag{mytag} for the basic setup, and then
tune some of the resulting low-level tag macros. As usual, the meaning of
Isabelle LaTeX output is determined by the user, by providing macros that
do the intended job. The default setup of Isabelle merely provides some
common cases as "canonical examples" that do some useful things. Just
check the generated tex sources together with the default sty files to get
the idea how it really works.
Makarius
Last updated: May 03 2024 at 08:18 UTC