--- 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"