1.1 --- a/NEWS	Tue Aug 16 12:51:07 2005 +0200
     1.2 +++ b/NEWS	Tue Aug 16 13:42:13 2005 +0200
     1.3 @@ -51,12 +51,25 @@
     1.4  and isatool print are used as front ends (these are subject to the
     1.5  DVI/PDF_VIEWER and PRINT_COMMAND settings, respectively).
     1.6  
     1.7 -* There is now a flag to control hiding of proofs and some other
     1.8 -commands (such as 'ML' or 'parse/print_translation') in document
     1.9 -output.  Hiding is enabled by default, and can be disabled by the
    1.10 -option '-H false' of isatool usedir or by resetting the reference
    1.11 -variable IsarOutput.hide_commands in ML.  Additional commands to be
    1.12 -hidden may be declared using IsarOutput.add_hidden_commands.
    1.13 +* Command tags control specific markup of certain regions of text,
    1.14 +notably folding and hiding.  Predefined tags include "theory" (for
    1.15 +theory begin and end), "proof" for proof commands, and "ML" for
    1.16 +commands involving ML code; the additional tags "visible" and
    1.17 +"invisible" are unused by default.  Users may give explicit tag
    1.18 +specifications in the text, e.g. ''by %invisible (auto)''.  The
    1.19 +interpretation of tags is determined by the LaTeX job during document
    1.20 +preparation: see option -V of isatool usedir, or options -n and -t of
    1.21 +isatool document, or even the LaTeX macros \isakeeptag, \isafoldtag,
    1.22 +\isadroptag.
    1.23 +
    1.24 +Several document versions may be produced at the same time via isatool
    1.25 +usedir (the generated index.html will link all of them).  Typical
    1.26 +specifications include ''-V document=theory,proof,ML'' to present
    1.27 +theory/proof/ML parts faithfully, ''-V outline=/proof,/ML'' to fold
    1.28 +proof and ML commands, and ''-V mutilated=-theory,-proof,-ML'' to omit
    1.29 +these parts without any formal replacement text.  The Isabelle site
    1.30 +default settings produce ''document'' and ''outline'' versions as
    1.31 +specified above.
    1.32  
    1.33  * Several new antiquotation:
    1.34