doc-src/IsarRef/generic.tex
changeset 24085 cbad32e7ab40
parent 24026 8a4d5312d378
child 24110 4ab3084e311c
     1.1 --- a/doc-src/IsarRef/generic.tex	Tue Jul 31 13:30:27 2007 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Tue Jul 31 13:30:35 2007 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  \chapter{Generic tools and packages}\label{ch:gen-tools}
     1.5  
     1.6 -\section{Theory specification commands}
     1.7 +\section{Specification commands}
     1.8  
     1.9  \subsection{Derived specifications}
    1.10  
    1.11 @@ -629,6 +629,44 @@
    1.12  \end{descr}
    1.13  
    1.14  
    1.15 +\subsection{Configuration options}
    1.16 +
    1.17 +Isabelle/Pure maintains a record of named configuration options within
    1.18 +the theory or proof context, with values of type $bool$, $int$, or
    1.19 +$string$.  Tools may declare options in ML, and then refer to these
    1.20 +values (relative to the context).  Thus global reference variables are
    1.21 +easily avoided.  The user may change the values of configuration
    1.22 +options by means of the $option$ attribute, which works particularly
    1.23 +well with commands such as $\isarkeyword{declare}$ or
    1.24 +$\isarkeyword{using}$.
    1.25 +
    1.26 +For historical reasons, some tools cannot take the full proof context
    1.27 +into account and merely refer to the background theory.  This is
    1.28 +accommodated by configuration options being declared as ``global'',
    1.29 +which may not be changed within a local context.
    1.30 +
    1.31 +\indexisaratt{option}\indexisarcmd{print-options}
    1.32 +\begin{matharray}{rcll}
    1.33 +  \isarcmd{print_options} & : & \isarkeep{theory~|~proof} \\
    1.34 +  option & : & \isaratt \\
    1.35 +\end{matharray}
    1.36 +
    1.37 +\begin{rail}
    1.38 +  'option' name ('=' ('true' | 'false' | int | name))?
    1.39 +\end{rail}
    1.40 +
    1.41 +\begin{descr}
    1.42 +
    1.43 +\item [$\isarkeyword{print_options}$] prints the available
    1.44 +  configuration options, with names, types, and current values.
    1.45 +
    1.46 +\item [$option~name = value$] modifies the named option, with the
    1.47 +  syntax of the value depending on the option's type.  For $bool$ the
    1.48 +  default value is $true$.  Any attempt to change a global option
    1.49 +  locally is ignored.
    1.50 +
    1.51 +\end{descr}
    1.52 +
    1.53  
    1.54  \section{Derived proof schemes}
    1.55