treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
authorwenzelm
Fri Sep 03 16:36:33 2010 +0200 (2010-09-03)
changeset 39117399977145846
parent 39116 f14735a88886
child 39118 12f3788be67b
treat show_free_types as plain ML option, without the extras of global default and registration in the attribute name space -- NB: 'print_configs' only shows the latter;
src/Pure/Isar/attrib.ML
src/Pure/Syntax/printer.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 16:09:12 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 16:36:33 2010 +0200
     1.3 @@ -392,8 +392,7 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val _ = Context.>> (Context.map_theory
     1.7 - (register_config Syntax.show_free_types_value #>
     1.8 -  register_config Syntax.show_question_marks_value #>
     1.9 + (register_config Syntax.show_question_marks_value #>
    1.10    register_config Goal_Display.show_consts_value #>
    1.11    register_config Unify.trace_bound_value #>
    1.12    register_config Unify.search_bound_value #>
     2.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 16:09:12 2010 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 16:36:33 2010 +0200
     2.3 @@ -9,8 +9,6 @@
     2.4    val show_brackets: bool Unsynchronized.ref
     2.5    val show_sorts: bool Unsynchronized.ref
     2.6    val show_types: bool Unsynchronized.ref
     2.7 -  val show_free_types_default: bool Unsynchronized.ref
     2.8 -  val show_free_types_value: Config.value Config.T
     2.9    val show_free_types: bool Config.T
    2.10    val show_all_types: bool Unsynchronized.ref
    2.11    val show_structs: bool Unsynchronized.ref
    2.12 @@ -56,10 +54,7 @@
    2.13  val show_all_types = Unsynchronized.ref false;
    2.14  val show_structs = Unsynchronized.ref false;
    2.15  
    2.16 -val show_free_types_default = Unsynchronized.ref true;
    2.17 -val show_free_types_value =
    2.18 -  Config.declare "show_free_types" (fn _ => Config.Bool (! show_free_types_default));
    2.19 -val show_free_types = Config.bool show_free_types_value;
    2.20 +val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    2.21  
    2.22  val show_question_marks_default = Unsynchronized.ref true;
    2.23  val show_question_marks_value =