# HG changeset patch
# User wenzelm
# Date 1283801599 -7200
# Node ID 4d701c0388c303b56d849830dfd3a2d9de07f747
# Parent  e6ec5283cd22819158f37bbb172596bfb4685e93
more explicit indication of Config.raw options, which are only needed for bootstrapping Pure;

diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -324,7 +324,7 @@
 
 structure Configs = Theory_Data
 (
-  type T = Config.value Config.T Symtab.table;
+  type T = Config.raw Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
   fun merge data = Symtab.merge (K true) data;
@@ -392,22 +392,22 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_brackets_value #>
-  register_config Syntax.show_sorts_value #>
-  register_config Syntax.show_types_value #>
-  register_config Syntax.show_structs_value #>
-  register_config Syntax.show_question_marks_value #>
-  register_config Syntax.ambiguity_level_value #>
-  register_config Syntax.eta_contract_value #>
-  register_config Goal_Display.goals_limit_value #>
-  register_config Goal_Display.show_main_goal_value #>
-  register_config Goal_Display.show_consts_value #>
-  register_config Unify.trace_bound_value #>
-  register_config Unify.search_bound_value #>
-  register_config Unify.trace_simp_value #>
-  register_config Unify.trace_types_value #>
-  register_config MetaSimplifier.simp_depth_limit_value #>
-  register_config MetaSimplifier.debug_simp_value #>
-  register_config MetaSimplifier.trace_simp_value));
+ (register_config Syntax.show_brackets_raw #>
+  register_config Syntax.show_sorts_raw #>
+  register_config Syntax.show_types_raw #>
+  register_config Syntax.show_structs_raw #>
+  register_config Syntax.show_question_marks_raw #>
+  register_config Syntax.ambiguity_level_raw #>
+  register_config Syntax.eta_contract_raw #>
+  register_config Goal_Display.goals_limit_raw #>
+  register_config Goal_Display.show_main_goal_raw #>
+  register_config Goal_Display.show_consts_raw #>
+  register_config Unify.trace_bound_raw #>
+  register_config Unify.search_bound_raw #>
+  register_config Unify.trace_simp_raw #>
+  register_config Unify.trace_types_raw #>
+  register_config MetaSimplifier.simp_depth_limit_raw #>
+  register_config MetaSimplifier.debug_simp_raw #>
+  register_config MetaSimplifier.trace_simp_raw));
 
 end;
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -7,20 +7,20 @@
 signature PRINTER0 =
 sig
   val show_brackets_default: bool Unsynchronized.ref
-  val show_brackets_value: Config.value Config.T
+  val show_brackets_raw: Config.raw
   val show_brackets: bool Config.T
   val show_types_default: bool Unsynchronized.ref
-  val show_types_value: Config.value Config.T
+  val show_types_raw: Config.raw
   val show_types: bool Config.T
   val show_sorts_default: bool Unsynchronized.ref
-  val show_sorts_value: Config.value Config.T
+  val show_sorts_raw: Config.raw
   val show_sorts: bool Config.T
   val show_free_types: bool Config.T
   val show_all_types: bool Config.T
-  val show_structs_value: Config.value Config.T
+  val show_structs_raw: Config.raw
   val show_structs: bool Config.T
   val show_question_marks_default: bool Unsynchronized.ref
-  val show_question_marks_value: Config.value Config.T
+  val show_question_marks_raw: Config.raw
   val show_question_marks: bool Config.T
 end;
 
@@ -55,28 +55,28 @@
 (** options for printing **)
 
 val show_brackets_default = Unsynchronized.ref false;
-val show_brackets_value =
+val show_brackets_raw =
   Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
-val show_brackets = Config.bool show_brackets_value;
+val show_brackets = Config.bool show_brackets_raw;
 
 val show_types_default = Unsynchronized.ref false;
-val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
-val show_types = Config.bool show_types_value;
+val show_types_raw = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
+val show_types = Config.bool show_types_raw;
 
 val show_sorts_default = Unsynchronized.ref false;
-val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
-val show_sorts = Config.bool show_sorts_value;
+val show_sorts_raw = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
+val show_sorts = Config.bool show_sorts_raw;
 
 val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
 val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
 
-val show_structs_value = Config.declare "show_structs" (fn _ => Config.Bool false);
-val show_structs = Config.bool show_structs_value;
+val show_structs_raw = Config.declare "show_structs" (fn _ => Config.Bool false);
+val show_structs = Config.bool show_structs_raw;
 
 val show_question_marks_default = Unsynchronized.ref true;
-val show_question_marks_value =
+val show_question_marks_raw =
   Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
-val show_question_marks = Config.bool show_question_marks_value;
+val show_question_marks = Config.bool show_question_marks_raw;
 
 
 
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/Syntax/syn_trans.ML
--- a/src/Pure/Syntax/syn_trans.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/Syntax/syn_trans.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -7,7 +7,7 @@
 signature SYN_TRANS0 =
 sig
   val eta_contract_default: bool Unsynchronized.ref
-  val eta_contract_value: Config.value Config.T
+  val eta_contract_raw: Config.raw
   val eta_contract: bool Config.T
   val atomic_abs_tr': string * typ * term -> term * term
   val preserve_binder_abs_tr': string -> string -> string * (term list -> term)
@@ -283,9 +283,8 @@
 (*do (partial) eta-contraction before printing*)
 
 val eta_contract_default = Unsynchronized.ref true;
-val eta_contract_value =
-  Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
-val eta_contract = Config.bool eta_contract_value;
+val eta_contract_raw = Config.declare "eta_contract" (fn _ => Config.Bool (! eta_contract_default));
+val eta_contract = Config.bool eta_contract_raw;
 
 fun eta_contr ctxt tm =
   let
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -111,7 +111,7 @@
   val print_syntax: syntax -> unit
   val guess_infix: syntax -> string -> mixfix option
   val ambiguity_enabled: bool Config.T
-  val ambiguity_level_value: Config.value Config.T
+  val ambiguity_level_raw: Config.raw
   val ambiguity_level: int Config.T
   val ambiguity_limit: int Config.T
   val standard_parse_term: (term -> string option) ->
@@ -694,8 +694,8 @@
 val ambiguity_enabled =
   Config.bool (Config.declare "syntax_ambiguity_enabled" (fn _ => Config.Bool true));
 
-val ambiguity_level_value = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
-val ambiguity_level = Config.int ambiguity_level_value;
+val ambiguity_level_raw = Config.declare "syntax_ambiguity_level" (fn _ => Config.Int 1);
+val ambiguity_level = Config.int ambiguity_level_raw;
 
 val ambiguity_limit =
   Config.int (Config.declare "syntax_ambiguity_limit" (fn _ => Config.Int 10));
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/config.ML
--- a/src/Pure/config.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/config.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -10,9 +10,10 @@
   val print_value: value -> string
   val print_type: value -> string
   type 'a T
-  val bool: value T -> bool T
-  val int: value T -> int T
-  val string: value T -> string T
+  type raw = value T
+  val bool: raw -> bool T
+  val int: raw -> int T
+  val string: raw -> string T
   val get: Proof.context -> 'a T -> 'a
   val map: 'a T -> ('a -> 'a) -> Proof.context -> Proof.context
   val put: 'a T -> 'a -> Proof.context -> Proof.context
@@ -22,9 +23,9 @@
   val get_generic: Context.generic -> 'a T -> 'a
   val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
   val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
-  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
-  val declare_global: string -> (Context.generic -> value) -> value T
-  val declare: string -> (Context.generic -> value) -> value T
+  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> raw
+  val declare_global: string -> (Context.generic -> value) -> raw
+  val declare: string -> (Context.generic -> value) -> raw
   val name_of: 'a T -> string
 end;
 
@@ -68,6 +69,8 @@
   get_value: Context.generic -> 'a,
   map_value: ('a -> 'a) -> Context.generic -> Context.generic};
 
+type raw = value T;
+
 fun coerce make dest (Config {name, get_value, map_value}) = Config
  {name = name,
   get_value = dest o get_value,
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/goal_display.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -8,14 +8,14 @@
 signature GOAL_DISPLAY =
 sig
   val goals_limit_default: int Unsynchronized.ref
-  val goals_limit_value: Config.value Config.T
+  val goals_limit_raw: Config.raw
   val goals_limit: int Config.T
   val goals_total: bool Config.T
   val show_main_goal_default: bool Unsynchronized.ref
-  val show_main_goal_value: Config.value Config.T
+  val show_main_goal_raw: Config.raw
   val show_main_goal: bool Config.T
   val show_consts_default: bool Unsynchronized.ref
-  val show_consts_value: Config.value Config.T
+  val show_consts_raw: Config.raw
   val show_consts: bool Config.T
   val pretty_flexpair: Proof.context -> term * term -> Pretty.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
@@ -26,19 +26,19 @@
 struct
 
 val goals_limit_default = Unsynchronized.ref 10;
-val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
-val goals_limit = Config.int goals_limit_value;
+val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
+val goals_limit = Config.int goals_limit_raw;
 
 val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
 
 val show_main_goal_default = Unsynchronized.ref false;
-val show_main_goal_value =
+val show_main_goal_raw =
   Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
-val show_main_goal = Config.bool show_main_goal_value;
+val show_main_goal = Config.bool show_main_goal_raw;
 
 val show_consts_default = Unsynchronized.ref false;
-val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
-val show_consts = Config.bool show_consts_value;
+val show_consts_raw = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
+val show_consts = Config.bool show_consts_raw;
 
 fun pretty_flexpair ctxt (t, u) = Pretty.block
   [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u];
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/meta_simplifier.ML
--- a/src/Pure/meta_simplifier.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/meta_simplifier.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -12,9 +12,9 @@
 signature BASIC_META_SIMPLIFIER =
 sig
   val debug_simp: bool Config.T
-  val debug_simp_value: Config.value Config.T
+  val debug_simp_raw: Config.raw
   val trace_simp: bool Config.T
-  val trace_simp_value: Config.value Config.T
+  val trace_simp_raw: Config.raw
   val trace_simp_default: bool Unsynchronized.ref
   val trace_simp_depth_limit: int Unsynchronized.ref
   type rrule
@@ -104,7 +104,7 @@
   val add_simp: thm -> simpset -> simpset
   val del_simp: thm -> simpset -> simpset
   val solver: simpset -> solver -> int -> tactic
-  val simp_depth_limit_value: Config.value Config.T
+  val simp_depth_limit_raw: Config.raw
   val simp_depth_limit: int Config.T
   val clear_ss: simpset -> simpset
   val simproc_global_i: theory -> string -> term list
@@ -250,8 +250,8 @@
 
 (* simp depth *)
 
-val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
-val simp_depth_limit = Config.int simp_depth_limit_value;
+val simp_depth_limit_raw = Config.declare "simp_depth_limit" (K (Config.Int 100));
+val simp_depth_limit = Config.int simp_depth_limit_raw;
 
 val trace_simp_depth_limit = Unsynchronized.ref 1;
 
@@ -273,12 +273,12 @@
 
 exception SIMPLIFIER of string * thm;
 
-val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
-val debug_simp = Config.bool debug_simp_value;
+val debug_simp_raw = Config.declare "debug_simp" (K (Config.Bool false));
+val debug_simp = Config.bool debug_simp_raw;
 
 val trace_simp_default = Unsynchronized.ref false;
-val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
-val trace_simp = Config.bool trace_simp_value;
+val trace_simp_raw = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
+val trace_simp = Config.bool trace_simp_raw;
 
 fun if_enabled (Simpset ({context, ...}, _)) flag f =
   (case context of
diff -r e6ec5283cd22 -r 4d701c0388c3 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Mon Sep 06 19:23:54 2010 +0200
+++ b/src/Pure/unify.ML	Mon Sep 06 21:33:19 2010 +0200
@@ -11,13 +11,13 @@
 
 signature UNIFY =
 sig
-  val trace_bound_value: Config.value Config.T
+  val trace_bound_raw: Config.raw
   val trace_bound: int Config.T
-  val search_bound_value: Config.value Config.T
+  val search_bound_raw: Config.raw
   val search_bound: int Config.T
-  val trace_simp_value: Config.value Config.T
+  val trace_simp_raw: Config.raw
   val trace_simp: bool Config.T
-  val trace_types_value: Config.value Config.T
+  val trace_types_raw: Config.raw
   val trace_types: bool Config.T
   val unifiers: theory * Envir.env * ((term * term) list) ->
     (Envir.env * (term * term) list) Seq.seq
@@ -32,20 +32,20 @@
 (*Unification options*)
 
 (*tracing starts above this depth, 0 for full*)
-val trace_bound_value = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
-val trace_bound = Config.int trace_bound_value;
+val trace_bound_raw = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
+val trace_bound = Config.int trace_bound_raw;
 
 (*unification quits above this depth*)
-val search_bound_value = Config.declare_global "unify_search_bound" (K (Config.Int 60));
-val search_bound = Config.int search_bound_value;
+val search_bound_raw = Config.declare_global "unify_search_bound" (K (Config.Int 60));
+val search_bound = Config.int search_bound_raw;
 
 (*print dpairs before calling SIMPL*)
-val trace_simp_value = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
-val trace_simp = Config.bool trace_simp_value;
+val trace_simp_raw = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
+val trace_simp = Config.bool trace_simp_raw;
 
 (*announce potential incompleteness of type unification*)
-val trace_types_value = Config.declare_global "unify_trace_types" (K (Config.Bool false));
-val trace_types = Config.bool trace_types_value;
+val trace_types_raw = Config.declare_global "unify_trace_types" (K (Config.Bool false));
+val trace_types = Config.bool trace_types_raw;
 
 
 type binderlist = (string*typ) list;