more explicit Config.declare vs. Config.declare_global;
authorwenzelm
Fri Sep 03 16:09:12 2010 +0200 (2010-09-03)
changeset 39116f14735a88886
parent 39115 a00da1674c1c
child 39117 399977145846
more explicit Config.declare vs. Config.declare_global;
src/Pure/Isar/attrib.ML
src/Pure/Syntax/printer.ML
src/Pure/config.ML
src/Pure/goal_display.ML
src/Pure/meta_simplifier.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 15:54:03 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 16:09:12 2010 +0200
     1.3 @@ -374,7 +374,7 @@
     1.4  
     1.5  fun declare_config make coerce global name default =
     1.6    let
     1.7 -    val config_value = Config.declare global name (make o default);
     1.8 +    val config_value = Config.declare_generic {global = global} name (make o default);
     1.9      val config = coerce config_value;
    1.10    in (config, register_config config_value) end;
    1.11  
     2.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 15:54:03 2010 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 16:09:12 2010 +0200
     2.3 @@ -58,12 +58,12 @@
     2.4  
     2.5  val show_free_types_default = Unsynchronized.ref true;
     2.6  val show_free_types_value =
     2.7 -  Config.declare false "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
     2.8 +  Config.declare "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
     2.9  val show_free_types = Config.bool show_free_types_value;
    2.10  
    2.11  val show_question_marks_default = Unsynchronized.ref true;
    2.12  val show_question_marks_value =
    2.13 -  Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    2.14 +  Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    2.15  val show_question_marks = Config.bool show_question_marks_value;
    2.16  
    2.17  fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
     3.1 --- a/src/Pure/config.ML	Fri Sep 03 15:54:03 2010 +0200
     3.2 +++ b/src/Pure/config.ML	Fri Sep 03 16:09:12 2010 +0200
     3.3 @@ -22,7 +22,9 @@
     3.4    val get_generic: Context.generic -> 'a T -> 'a
     3.5    val map_generic: 'a T -> ('a -> 'a) -> Context.generic -> Context.generic
     3.6    val put_generic: 'a T -> 'a -> Context.generic -> Context.generic
     3.7 -  val declare: bool -> string -> (Context.generic -> value) -> value T
     3.8 +  val declare_generic: {global: bool} -> string -> (Context.generic -> value) -> value T
     3.9 +  val declare_global: string -> (Context.generic -> value) -> value T
    3.10 +  val declare: string -> (Context.generic -> value) -> value T
    3.11    val name_of: 'a T -> string
    3.12  end;
    3.13  
    3.14 @@ -98,7 +100,7 @@
    3.15    fun merge data = Inttab.merge (K true) data;
    3.16  );
    3.17  
    3.18 -fun declare global name default =
    3.19 +fun declare_generic {global} name default =
    3.20    let
    3.21      val id = serial ();
    3.22  
    3.23 @@ -120,6 +122,9 @@
    3.24        | map_value f context = update_value f context;
    3.25    in Config {name = name, get_value = get_value, map_value = map_value} end;
    3.26  
    3.27 +val declare_global = declare_generic {global = true};
    3.28 +val declare = declare_generic {global = false};
    3.29 +
    3.30  fun name_of (Config {name, ...}) = name;
    3.31  
    3.32  
     4.1 --- a/src/Pure/goal_display.ML	Fri Sep 03 15:54:03 2010 +0200
     4.2 +++ b/src/Pure/goal_display.ML	Fri Sep 03 16:09:12 2010 +0200
     4.3 @@ -24,8 +24,7 @@
     4.4  
     4.5  (*true: show consts with types in proof state output*)
     4.6  val show_consts_default = Unsynchronized.ref false;
     4.7 -val show_consts_value =
     4.8 -  Config.declare false "show_consts" (fn _ => Config.Bool (! show_consts_default));
     4.9 +val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default));
    4.10  val show_consts = Config.bool show_consts_value;
    4.11  
    4.12  fun pretty_flexpair ctxt (t, u) = Pretty.block
     5.1 --- a/src/Pure/meta_simplifier.ML	Fri Sep 03 15:54:03 2010 +0200
     5.2 +++ b/src/Pure/meta_simplifier.ML	Fri Sep 03 16:09:12 2010 +0200
     5.3 @@ -250,7 +250,7 @@
     5.4  
     5.5  (* simp depth *)
     5.6  
     5.7 -val simp_depth_limit_value = Config.declare false "simp_depth_limit" (K (Config.Int 100));
     5.8 +val simp_depth_limit_value = Config.declare "simp_depth_limit" (K (Config.Int 100));
     5.9  val simp_depth_limit = Config.int simp_depth_limit_value;
    5.10  
    5.11  val trace_simp_depth_limit = Unsynchronized.ref 1;
    5.12 @@ -273,12 +273,11 @@
    5.13  
    5.14  exception SIMPLIFIER of string * thm;
    5.15  
    5.16 -val debug_simp_value = Config.declare false "debug_simp" (K (Config.Bool false));
    5.17 +val debug_simp_value = Config.declare "debug_simp" (K (Config.Bool false));
    5.18  val debug_simp = Config.bool debug_simp_value;
    5.19  
    5.20  val trace_simp_default = Unsynchronized.ref false;
    5.21 -val trace_simp_value =
    5.22 -  Config.declare false "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
    5.23 +val trace_simp_value = Config.declare "trace_simp" (fn _ => Config.Bool (! trace_simp_default));
    5.24  val trace_simp = Config.bool trace_simp_value;
    5.25  
    5.26  fun if_enabled (Simpset ({context, ...}, _)) flag f =
     6.1 --- a/src/Pure/unify.ML	Fri Sep 03 15:54:03 2010 +0200
     6.2 +++ b/src/Pure/unify.ML	Fri Sep 03 16:09:12 2010 +0200
     6.3 @@ -32,19 +32,19 @@
     6.4  (*Unification options*)
     6.5  
     6.6  (*tracing starts above this depth, 0 for full*)
     6.7 -val trace_bound_value = Config.declare true "unify_trace_bound" (K (Config.Int 50));
     6.8 +val trace_bound_value = Config.declare_global "unify_trace_bound" (K (Config.Int 50));
     6.9  val trace_bound = Config.int trace_bound_value;
    6.10  
    6.11  (*unification quits above this depth*)
    6.12 -val search_bound_value = Config.declare true "unify_search_bound" (K (Config.Int 60));
    6.13 +val search_bound_value = Config.declare_global "unify_search_bound" (K (Config.Int 60));
    6.14  val search_bound = Config.int search_bound_value;
    6.15  
    6.16  (*print dpairs before calling SIMPL*)
    6.17 -val trace_simp_value = Config.declare true "unify_trace_simp" (K (Config.Bool false));
    6.18 +val trace_simp_value = Config.declare_global "unify_trace_simp" (K (Config.Bool false));
    6.19  val trace_simp = Config.bool trace_simp_value;
    6.20  
    6.21  (*announce potential incompleteness of type unification*)
    6.22 -val trace_types_value = Config.declare true "unify_trace_types" (K (Config.Bool false));
    6.23 +val trace_types_value = Config.declare_global "unify_trace_types" (K (Config.Bool false));
    6.24  val trace_types = Config.bool trace_types_value;
    6.25  
    6.26