Re: [isabelle] Folding additional tags?



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.