*To*: Peter Sewell <Peter.Sewell at cl.cam.ac.uk>*Subject*: Re: [isabelle] quoting definitions in latex*From*: Makarius <makarius at sketis.net>*Date*: Fri, 14 Dec 2007 20:39:44 +0100 (CET)*Cc*: isabelle-users at cl.cam.ac.uk*In-reply-to*: <E1J3FdJ-00060V-00@mta2.cl.cam.ac.uk>*References*: <E1J38zt-0004OF-00@mta2.cl.cam.ac.uk> <4762AA98.1060200@in.tum.de> <E1J3E5N-0003yZ-00@mta2.cl.cam.ac.uk> <4762BD56.2090104@in.tum.de> <Pine.LNX.4.63.0712141943040.30639@atbroy101.informatik.tu-muenchen.de> <E1J3FdJ-00060V-00@mta2.cl.cam.ac.uk>

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. Makarius

**References**:**[isabelle] quoting definitions in latex***From:*Peter Sewell

**Re: [isabelle] quoting definitions in latex***From:*Tobias Nipkow

**Re: [isabelle] quoting definitions in latex***From:*Peter Sewell

- Previous by Date: Re: [isabelle] quoting definitions in latex
- Next by Date: Re: [isabelle] Modifying theorems
- Previous by Thread: Re: [isabelle] quoting definitions in latex
- Next by Thread: Re: [isabelle] quoting definitions in latex
- Cl-isabelle-users December 2007 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list