Re: [isabelle] quoting definitions in latex

On Fri, 14 Dec 2007, Peter Sewell wrote:

> into
>   \newcommand{\myisadatatypeXXXdirn}{dirn\ {\isacharequal}\ R\ {\isacharbar}\ W}

This does not work in general, because the presentation system does not 
know about the syntax of individual commands.  Even if we pretend to know 
the particular datatype syntax, what happens with mutual datatype 
definitions, for example?

> Then the user can LaTeX-include the first file and write just
>   \myisadatatypeXXXdirn
> whereever they need to quote that defn.

This also does not work, because specifications of name bindings do not 
identify the resulting internal object uniquely.  E.g. there could be 
several "dirn" types in different name spaces, local scopes etc.

The Isabelle document preparation might look crude at first sight, but it 
is indeed very sophisticated: it manages to get 99% of typesetting quality 
with only 1% of knowledge about the structure of the sources.

See also chapter 2 of the Isabelle system manual for the general 
explanation on how things really work.  The gory details can then be 
glimpsed from the Isabelle style files and the generated LaTeX.

If you really want to move around portions of typeset text, you can try to 
find a LaTeX package that allows to move marked regions.  You can then let 
Isabelle insert the required markup either via the 'text_raw' command or 
using the new %tag facility, which is also explained in the manual.


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