--- a/doc-src/IsarRef/generic.tex Wed Aug 01 16:50:16 2007 +0200
+++ b/doc-src/IsarRef/generic.tex Wed Aug 01 16:55:37 2007 +0200
@@ -631,13 +631,13 @@
\subsection{Configuration options}
-Isabelle/Pure maintains a record of named configuration options within
-the theory or proof context, with values of type $bool$, $int$, or
-$string$. Tools may declare options in ML, and then refer to these
-values (relative to the context). Thus global reference variables are
-easily avoided. The user may change the values of configuration
-options by means of the $option$ attribute, which works particularly
-well with commands such as $\isarkeyword{declare}$ or
+Isabelle/Pure maintains a record of named configuration options within the
+theory or proof context, with values of type $bool$, $int$, or $string$.
+Tools may declare options in ML, and then refer to these values (relative to
+the context). Thus global reference variables are easily avoided. The user
+may change the value of a configuration option by means of an associated
+attribute of the same name. This form of context declaration works
+particularly well with commands such as $\isarkeyword{declare}$ or
$\isarkeyword{using}$.
For historical reasons, some tools cannot take the full proof context
@@ -645,25 +645,24 @@
accommodated by configuration options being declared as ``global'',
which may not be changed within a local context.
-\indexisaratt{option}\indexisarcmd{print-options}
+\indexisarcmd{print-configs}
\begin{matharray}{rcll}
- \isarcmd{print_options} & : & \isarkeep{theory~|~proof} \\
- option & : & \isaratt \\
+ \isarcmd{print_configs} & : & \isarkeep{theory~|~proof} \\
\end{matharray}
\begin{rail}
- 'option' name ('=' ('true' | 'false' | int | name))?
+ name ('=' ('true' | 'false' | int | name))?
\end{rail}
\begin{descr}
-
-\item [$\isarkeyword{print_options}$] prints the available
- configuration options, with names, types, and current values.
-
-\item [$option~name = value$] modifies the named option, with the
- syntax of the value depending on the option's type. For $bool$ the
- default value is $true$. Any attempt to change a global option
- locally is ignored.
+
+\item [$\isarkeyword{print_configs}$] prints the available configuration
+ options, with names, types, and current values.
+
+\item [$name = value$] as an attribute expression modifies the named option,
+ with the syntax of the value depending on the option's type. For $bool$ the
+ default value is $true$. Any attempt to change a global option in a local
+ context is ignored.
\end{descr}