--- a/NEWS Wed Aug 01 16:50:16 2007 +0200
+++ b/NEWS Wed Aug 01 16:55:37 2007 +0200
@@ -164,19 +164,21 @@
* Configuration options are maintained within the theory or proof
context (with name and type bool/int/string), providing a very simple
interface to a poor-man's version of general context data. Tools may
-declare options in ML (e.g. using ConfigOption.int) and then refer to
-these values using ConfigOption.get etc. Users may change options via
-the "option" attribute, which works particularly well with commands
-'declare' or 'using', for example ``declare [[option foo = 42]]''.
-Thus global reference variables are easily avoided, which do not
-observe Isar toplevel undo/redo and fail to work with multithreading.
+declare options in ML (e.g. using Attrib.config_int) and then refer to
+these values using Config.get etc. Users may change options via an
+associated attribute of the same name. This form of context
+declaration works particularly well with commands 'declare' or
+'using', for example ``declare [[foo = 42]]''. Thus it has become
+very easy to avoid global references, which would not observe Isar
+toplevel undo/redo and fail to work with multithreading.
* Named collections of theorems may be easily installed as context
data using the functor NamedThmsFun (see
src/Pure/Tools/named_thms.ML). The user may add or delete facts via
-attributes. This is just a common case of general context data, which
-is the preferred way for anything more complex than just a list of
-facts in canonical order.
+attributes; there is also a toplevel print command. This facility is
+just a common case of general context data, which is the preferred way
+for anything more complex than just a list of facts in canonical
+order.
* Isar: command 'declaration' augments a local theory by generic
declaration functions written in ML. This enables arbitrary content
--- a/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 01 16:50:16 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/ML.thy Wed Aug 01 16:55:37 2007 +0200
@@ -196,8 +196,9 @@
\secref{sec:context-data}) there are drop-in replacements that
emulate primitive references for common cases of \emph{configuration
options} for type @{ML_type "bool"}/@{ML_type "int"}/@{ML_type
- "string"} (see structure @{ML_struct ConfigOption}) and lists of
- theorems (see functor @{ML_functor NamedThmsFun}).
+ "string"} (see structure @{ML_struct Config} and @{ML
+ Attrib.config_bool} etc.), and lists of theorems (see functor
+ @{ML_functor NamedThmsFun}).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
--- a/doc-src/IsarImplementation/Thy/document/ML.tex Wed Aug 01 16:50:16 2007 +0200
+++ b/doc-src/IsarImplementation/Thy/document/ML.tex Wed Aug 01 16:55:37 2007 +0200
@@ -217,8 +217,8 @@
from the fully general functors for theory and proof data (see
\secref{sec:context-data}) there are drop-in replacements that
emulate primitive references for common cases of \emph{configuration
- options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|ConfigOption|) and lists of
- theorems (see functor \verb|NamedThmsFun|).
+ options} for type \verb|bool|/\verb|int|/\verb|string| (see structure \verb|Config| and \verb|Attrib.config_bool| etc.), and lists of theorems (see functor
+ \verb|NamedThmsFun|).
\item Keep components with local state information
\emph{re-entrant}. Instead of poking initial values into (private)
--- 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}
--- a/src/HOL/HoareParallel/Graph.thy Wed Aug 01 16:50:16 2007 +0200
+++ b/src/HOL/HoareParallel/Graph.thy Wed Aug 01 16:55:37 2007 +0200
@@ -173,9 +173,9 @@
prefer 2 apply arith
apply(drule_tac n = "Suc nata" in Compl_lemma)
apply clarify
- using [[option fast_arith_split_limit = 0]]
+ using [[fast_arith_split_limit = 0]]
apply force
- using [[option fast_arith_split_limit = 9]]
+ using [[fast_arith_split_limit = 9]]
apply(drule leI)
apply(subgoal_tac "Suc (length path - Suc m + nata)=(length path - Suc 0) - (m - Suc nata)")
apply(erule_tac x = "m - (Suc nata)" in allE)
--- a/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:50:16 2007 +0200
+++ b/src/HOL/MicroJava/Comp/CorrCompTp.thy Wed Aug 01 16:55:37 2007 +0200
@@ -454,7 +454,7 @@
apply (simp add: max_of_list_def)
apply (induct xs)
apply simp
-using [[option fast_arith_split_limit = 0]]
+using [[fast_arith_split_limit = 0]]
apply simp
apply arith
done
--- a/src/HOL/Nominal/nominal_package.ML Wed Aug 01 16:50:16 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Wed Aug 01 16:55:37 2007 +0200
@@ -880,10 +880,10 @@
(* prove distinctness theorems *)
- val distinctness_limit = ConfigOption.get_thy thy8 DatatypeProp.distinctness_limit;
- val thy8' = ConfigOption.put_thy DatatypeProp.distinctness_limit 1000 thy8;
+ val distinctness_limit = Config.get_thy thy8 DatatypeProp.distinctness_limit;
+ val thy8' = Config.put_thy DatatypeProp.distinctness_limit 1000 thy8;
val distinct_props = DatatypeProp.make_distincts new_type_names descr' sorts' thy8';
- val thy8 = ConfigOption.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
+ val thy8 = Config.put_thy DatatypeProp.distinctness_limit distinctness_limit thy8';
val dist_rewrites = map (fn (rep_thms, dist_lemma) =>
dist_lemma::(rep_thms @ [In0_eq, In1_eq, In0_not_In1, In1_not_In0]))
--- a/src/Pure/Isar/attrib.ML Wed Aug 01 16:50:16 2007 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 01 16:55:37 2007 +0200
@@ -26,6 +26,14 @@
(('c * 'att list) * ('d * 'att list) list) list
val crude_closure: Proof.context -> src -> src
val add_attributes: (bstring * (src -> attribute) * string) list -> theory -> theory
+ val print_configs: Proof.context -> unit
+ val register_config: bstring -> Config.value Config.T -> theory -> theory
+ val config_bool: bstring -> bool -> bool Config.T * (theory -> theory)
+ val config_int: bstring -> int -> int Config.T * (theory -> theory)
+ val config_string: bstring -> string -> string Config.T * (theory -> theory)
+ val config_bool_global: bstring -> bool -> bool Config.T * (theory -> theory)
+ val config_int_global: bstring -> int -> int Config.T * (theory -> theory)
+ val config_string_global: bstring -> string -> string Config.T * (theory -> theory)
val thm: Context.generic * Args.T list -> thm * (Context.generic * Args.T list)
val thms: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
val multi_thm: Context.generic * Args.T list -> thm list * (Context.generic * Args.T list)
@@ -46,7 +54,7 @@
(* theory data *)
-structure AttributesData = TheoryDataFun
+structure Attributes = TheoryDataFun
(
type T = (((src -> attribute) * string) * stamp) NameSpace.table;
val empty = NameSpace.empty_table;
@@ -58,7 +66,7 @@
fun print_attributes thy =
let
- val attribs = AttributesData.get thy;
+ val attribs = Attributes.get thy;
fun prt_attr (name, ((_, comment), _)) = Pretty.block
[Pretty.str (name ^ ":"), Pretty.brk 2, Pretty.str comment];
in
@@ -69,10 +77,10 @@
(* name space *)
-val intern = NameSpace.intern o #1 o AttributesData.get;
+val intern = NameSpace.intern o #1 o Attributes.get;
val intern_src = Args.map_name o intern;
-val extern = NameSpace.extern o #1 o AttributesData.get o ProofContext.theory_of;
+val extern = NameSpace.extern o #1 o Attributes.get o ProofContext.theory_of;
(* pretty printing *)
@@ -87,7 +95,7 @@
fun attribute_i thy =
let
- val attrs = #2 (AttributesData.get thy);
+ val attrs = #2 (Attributes.get thy);
fun attr src =
let val ((name, _), pos) = Args.dest_src src in
(case Symtab.lookup attrs name of
@@ -125,7 +133,7 @@
raw_attrs |> map (fn (name, att, comment) => (name, ((att, comment), stamp ())));
fun add attrs = NameSpace.extend_table (Sign.naming_of thy) new_attrs attrs
handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
- in AttributesData.map add thy end;
+ in Attributes.map add thy end;
@@ -188,39 +196,76 @@
-(** basic attributes **)
+(** configuration options **)
+
+(* naming *)
+
+structure Configs = TheoryDataFun
+(struct
+ type T = Config.value Config.T Symtab.table;
+ val empty = Symtab.empty;
+ val copy = I;
+ val extend = I;
+ fun merge _ = Symtab.merge (K true);
+end);
-(* configuration options *)
+fun print_configs ctxt =
+ let
+ val thy = ProofContext.theory_of ctxt;
+ fun prt (name, config) =
+ let val value = Config.get ctxt config in
+ Pretty.block [Pretty.str (name ^ ": " ^ Config.print_type value ^ " ="), Pretty.brk 1,
+ Pretty.str (Config.print_value value)]
+ end;
+ val configs = NameSpace.extern_table (#1 (Attributes.get thy), Configs.get thy);
+ in Pretty.writeln (Pretty.big_list "configuration options" (map prt configs)) end;
+
+
+(* concrete syntax *)
local
val equals = Args.$$$ "=";
-fun scan_value (ConfigOption.Bool _) =
- (equals -- Args.$$$ "false") >> K (ConfigOption.Bool false) ||
- (equals -- Args.$$$ "true") >> K (ConfigOption.Bool true) ||
- (Scan.succeed (ConfigOption.Bool true))
- | scan_value (ConfigOption.Int _) = (equals |-- Args.int) >> ConfigOption.Int
- | scan_value (ConfigOption.String _) = (equals |-- Args.name) >> ConfigOption.String;
+fun scan_value (Config.Bool _) =
+ equals -- Args.$$$ "false" >> K (Config.Bool false) ||
+ equals -- Args.$$$ "true" >> K (Config.Bool true) ||
+ Scan.succeed (Config.Bool true)
+ | scan_value (Config.Int _) = equals |-- Args.int >> Config.Int
+ | scan_value (Config.String _) = equals |-- Args.name >> Config.String;
-fun scan_config thy =
- (Args.name >> ConfigOption.the_option thy) :|-- (fn (config, config_type) =>
- scan_value config_type >> (fn value =>
- K (Thm.declaration_attribute (K (ConfigOption.put_generic config value)))));
-
-fun scan_att thy =
- (Args.internal_attribute ||
- (Scan.ahead (scan_config thy --| Args.terminator) :|--
- (fn att => Args.named_attribute (K att))));
+fun scan_config thy config =
+ let val config_type = Config.get_thy thy config
+ in scan_value config_type >> (K o Thm.declaration_attribute o K o Config.put_generic config) end;
in
-fun option x = syntax (Scan.peek (fn context =>
- (scan_att (Context.theory_of context) >> Morphism.form) --| Scan.many Args.not_eof)) x;
+fun register_config name config thy =
+ thy
+ |> add_attributes
+ [(name, syntax (Scan.lift (scan_config thy config) >> Morphism.form), "configuration option")]
+ |> Configs.map (Symtab.update (Sign.full_name thy name, config));
+
+fun declare_config make coerce global name default =
+ let
+ val config_value = Config.declare global name (make default);
+ val config = coerce config_value;
+ in (config, register_config name config_value) end;
+
+val config_bool = declare_config Config.Bool Config.bool false;
+val config_int = declare_config Config.Int Config.int false;
+val config_string = declare_config Config.String Config.string false;
+
+val config_bool_global = declare_config Config.Bool Config.bool true;
+val config_int_global = declare_config Config.Int Config.int true;
+val config_string_global = declare_config Config.String Config.string true;
end;
+
+(** basic attributes **)
+
(* tags *)
fun tagged x = syntax (tag >> PureThy.tag) x;
@@ -300,8 +345,7 @@
val _ = Context.add_setup
(add_attributes
- [("option", option, "named configuration option"),
- ("tagged", tagged, "tagged theorem"),
+ [("tagged", tagged, "tagged theorem"),
("untagged", untagged, "untagged theorem"),
("kind", kind, "theorem kind"),
("COMP", COMP_att, "direct composition with rules (no lifting)"),