Re: [isabelle] Where is isatool usedir -H ?



Hi Nicole,

this has been enhanced in the development version (and also in the
upcoming Isabelle2005, of course). A short introduction:

> * Command tags control specific markup of certain regions of text, notably
> folding and hiding.  Predefined tags include "theory" (for theory begin
> and end), "proof" for proof commands, and "ML" for commands involving ML
> code; the additional tags "visible" and "invisible" are unused by
> default.  Users may give explicit tag specifications in the text, e.g.
> ''by %invisible (auto)''.  The interpretation of tags is determined by
> the LaTeX job during document preparation: see option -V of isatool
> usedir, or options -n and -t of isatool document, or even the LaTeX
> macros \isakeeptag, \isafoldtag, \isadroptag.
>
> Several document versions may be produced at the same time via isatool
> usedir (the generated index.html will link all of them).  Typical
> specifications include ''-V document=theory,proof,ML'' to present
> theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold proof
> and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit these
> parts without any formal replacement text.  The Isabelle site default
> settings produce ''document'' and ''outline'' versions as specified above.

> (This concept replaces the -H option of usedir.)

Hope this helps
Florian

--

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
begin:vcard
fn:Florian Haftmann
n:Haftmann;Florian
org;quoted-printable;quoted-printable:Technische Universit=C3=A4t M=C3=BCnchen ;Institut f=C3=BCr Informatik, Lehrstuhl Software and Systems Engineering
adr;quoted-printable;quoted-printable:;;Boltzmannstra=C3=9Fe 3;M=C3=BCnchen;Bayern;85748;Deutschland
email;internet:florian.haftmann at informatik.tu-muenchen.de
title:M. Sc.
tel;work:(++49 89) 289 - 17300
note;quoted-printable:PGP available: =
	=0D=0A=
	http://www4.informatik.tu-muenchen.de/~haftmann/pgp/florian_haftmann_at_i=
	nformatik_tu_muenchen_de.pgp=0D=0A=

x-mozilla-html:FALSE
url:http://isabelle.in.tum.de/~haftmann
version:2.1
end:vcard

Attachment: signature.asc
Description: OpenPGP digital signature



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