1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Nov 13 21:32:36 2008 +0100
     1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy	Thu Nov 13 21:33:15 2008 +0100
     1.3 @@ -396,10 +396,11 @@
     1.4  *}
     1.5  
     1.6  
     1.7 -section {* Tagged commands \label{sec:tags} *}
     1.8 +section {* Markup via command tags \label{sec:tags} *}
     1.9  
    1.10 -text {*
    1.11 -  Each Isabelle/Isar command may be decorated by presentation tags:
    1.12 +text {* Each Isabelle/Isar command may be decorated by additional
    1.13 +  presentation tags, to indicate some modification in the way it is
    1.14 +  printed in the document.
    1.15  
    1.16    \indexouternonterm{tags}
    1.17    \begin{rail}
    1.18 @@ -408,34 +409,43 @@
    1.19      tag: '\%' (ident | string)
    1.20    \end{rail}
    1.21  
    1.22 -  The tags @{text "theory"}, @{text "proof"}, @{text "ML"} are already
    1.23 -  pre-declared for certain classes of commands:
    1.24 +  Some tags are pre-declared for certain classes of commands, serving
    1.25 +  as default markup if no tags are given in the text:
    1.26  
    1.27 - \medskip
    1.28 -
    1.29 +  \medskip
    1.30    \begin{tabular}{ll}
    1.31      @{text "theory"} & theory begin/end \\
    1.32      @{text "proof"} & all proof commands \\
    1.33      @{text "ML"} & all commands involving ML code \\
    1.34    \end{tabular}
    1.35  
    1.36 -  \medskip The Isabelle document preparation system (see also
    1.37 -  \cite{isabelle-sys}) allows tagged command regions to be presented
    1.38 +  \medskip The Isabelle document preparation system
    1.39 +  \cite{isabelle-sys} allows tagged command regions to be presented
    1.40    specifically, e.g.\ to fold proof texts, or drop parts of the text
    1.41    completely.
    1.42  
    1.43 -  For example ``@{command "by"}~@{text "%invisible auto"}'' would
    1.44 -  cause that piece of proof to be treated as @{text invisible} instead
    1.45 -  of @{text "proof"} (the default), which may be either show or hidden
    1.46 +  For example ``@{command "by"}~@{text "%invisible auto"}'' causes
    1.47 +  that piece of proof to be treated as @{text invisible} instead of
    1.48 +  @{text "proof"} (the default), which may be shown or hidden
    1.49    depending on the document setup.  In contrast, ``@{command
    1.50 -  "by"}~@{text "%visible auto"}'' would force this text to be shown
    1.51 +  "by"}~@{text "%visible auto"}'' forces this text to be shown
    1.52    invariably.
    1.53  
    1.54    Explicit tag specifications within a proof apply to all subsequent
    1.55    commands of the same level of nesting.  For example, ``@{command
    1.56 -  "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' would force the
    1.57 -  whole sub-proof to be typeset as @{text visible} (unless some of its
    1.58 -  parts are tagged differently).
    1.59 +  "proof"}~@{text "%visible \<dots>"}~@{command "qed"}'' forces the whole
    1.60 +  sub-proof to be typeset as @{text visible} (unless some of its parts
    1.61 +  are tagged differently).
    1.62 +
    1.63 +  \medskip Command tags merely produce certain markup environments for
    1.64 +  type-setting.  The meaning of these is determined by {\LaTeX}
    1.65 +  macros, as defined in @{"file" "~~/lib/texinputs/isabelle.sty"} or
    1.66 +  by the document author.  The Isabelle document preparation tools
    1.67 +  also provide some high-level options to specify the meaning of
    1.68 +  arbitrary tags to ``keep'', ``drop'', or ``fold'' the corresponding
    1.69 +  parts of the text.  Logic sessions may also specify ``document
    1.70 +  versions'', where given tags are interpreted in some particular way.
    1.71 +  Again see \cite{isabelle-sys} for further details.
    1.72  *}
    1.73  
    1.74