# HG changeset patch
# User wenzelm
# Date 1124192539 -7200
# Node ID 80fceeb2bcef855b7c18f672b04f07d7379eed50
# Parent  30781cc78fc692a092c4552497f12abc5c001152
tuned antiquotations;
added tagged commands;

diff -r 30781cc78fc6 -r 80fceeb2bcef doc-src/IsarRef/syntax.tex
--- a/doc-src/IsarRef/syntax.tex	Tue Aug 16 13:42:18 2005 +0200
+++ b/doc-src/IsarRef/syntax.tex	Tue Aug 16 13:42:19 2005 +0200
@@ -410,15 +410,21 @@
 
 \subsection{Antiquotations}\label{sec:antiq}
 
-\begin{matharray}{rcl@{\hspace*{2cm}}rcl}
-  thm & : & \isarantiq & text & : & \isarantiq \\
-  prop & : & \isarantiq & goals & : & \isarantiq \\
-  term & : & \isarantiq & subgoals & : & \isarantiq \\
-  const & : & \isarantiq & prf & : & \isarantiq \\
-  typeof & : & \isarantiq & full_prf & : & \isarantiq \\
-  typ & : & \isarantiq \\  
-  thm_style & : & \isarantiq \\  
-  term_style & : & \isarantiq \\  
+\begin{matharray}{rcl}
+  thm & : & \isarantiq \\
+  prop & : & \isarantiq \\
+  term & : & \isarantiq \\
+  const & : & \isarantiq \\
+  typeof & : & \isarantiq \\
+  typ & : & \isarantiq \\
+  thm_style & : & \isarantiq \\
+  term_style & : & \isarantiq \\
+  text & : & \isarantiq \\
+  goals & : & \isarantiq \\
+  subgoals & : & \isarantiq \\
+  prf & : & \isarantiq \\
+  full_prf & : & \isarantiq \\
+  ML & : & \isarantiq \\
 \end{matharray}
 
 The text body of formal comments (see also \S\ref{sec:comments}) may contain
@@ -439,7 +445,7 @@
 \indexisarant{thm}\indexisarant{prop}\indexisarant{term}\indexisarant{const}
 \indexisarant{typeof}\indexisarant{typ}\indexisarant{thm-style}
 \indexisarant{term-style}\indexisarant{text}\indexisarant{goals}
-\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}
+\indexisarant{subgoals}\indexisarant{prf}\indexisarant{full-prf}\indexisarant{ML}
 
 \begin{rail}
   atsign lbrace antiquotation rbrace
@@ -452,13 +458,14 @@
     'const' options term |
     'typeof' options term |
     'typ' options type |
-    'thm\_style' options style thmref |
-    'term\_style' options style term |
+    'thm\_style' options name thmref |
+    'term\_style' options name term |
     'text' options name |
     'goals' options |
     'subgoals' options |
     'prf' options thmrefs |
-    'full\_prf' options thmrefs
+    'full\_prf' options thmrefs |
+    'ML' options name
   ;
   options: '[' (option * ',') ']'
   ;
@@ -514,6 +521,9 @@
 \item [$\at\{full_prf~\vec a\}$] is like $\at\{prf~\vec a\}$, but displays the
   full proof terms, i.e.\ also displays information omitted in the compact
   proof term, which is denoted by ``$_$'' placeholders there.
+  
+\item [$\at\{ML~s\}$] checks text $s$ as an ML expression in the current
+  runtime environment, and displays the source verbatim.
 
 \end{descr}
 
@@ -587,6 +597,43 @@
 well-formedness of terms and types with respect to the current theory or proof
 context is ensured here.
 
+
+\subsection{Tagged commands}\label{sec:tags}
+
+Each Isabelle/Isar command may be decorated by presentation tags:
+
+\indexouternonterm{tags}
+\begin{rail}
+  tags: ( tag * )
+  ;
+  tag: '\%' (ident | string)
+\end{rail}
+
+The tags $theory$, $proof$, $ML$ are already pre-declared for certain classes
+of commands:
+
+\medskip
+
+\begin{tabular}{ll}
+  $theory$ & theory begin and end \\
+  $proof$ & all proof commands \\
+  $ML$ & all commands involving ML code \\
+\end{tabular}
+
+\medskip The Isabelle document preparation system (see also
+\cite{isabelle-sys}) allows tagged command regions to be presented
+specifically, e.g.\ to fold proof texts, or drop parts of the text completely.
+
+For example ``$\BYNAME~\%invisible~(auto)$'' would cause that piece of proof
+to be treated as $invisible$ instead of $proof$ (the default), which may be
+either show or hidden depending on the document setup.  In contrast,
+``$\BYNAME~\%visible~(auto)$'' would force this text to be shown invariably.
+
+Explicit tag specifications within a proof apply to all subsequent commands of
+the same level of nesting.  For example,
+``$\PROOFNAME~\%visible~\dots\QEDNAME$'' would force the whole sub-proof to be
+typeset as $visible$ (unless some of its parts are tagged differently).
+
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "isar-ref"