turned show_structs into proper configuration option;
authorwenzelm
Fri Sep 03 22:57:21 2010 +0200 (2010-09-03)
changeset 39127e7ecbe86d22e
parent 39126 ee117c5b3b75
child 39128 93a7365fb4ee
turned show_structs into proper configuration option;
src/Pure/Isar/attrib.ML
src/Pure/Syntax/printer.ML
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Fri Sep 03 22:36:16 2010 +0200
     1.2 +++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 22:57:21 2010 +0200
     1.3 @@ -392,7 +392,8 @@
     1.4  (* theory setup *)
     1.5  
     1.6  val _ = Context.>> (Context.map_theory
     1.7 - (register_config Syntax.show_question_marks_value #>
     1.8 + (register_config Syntax.show_structs_value #>
     1.9 +  register_config Syntax.show_question_marks_value #>
    1.10    register_config Syntax.ambiguity_level_value #>
    1.11    register_config Goal_Display.goals_limit_value #>
    1.12    register_config Goal_Display.show_main_goal_value #>
     2.1 --- a/src/Pure/Syntax/printer.ML	Fri Sep 03 22:36:16 2010 +0200
     2.2 +++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 22:57:21 2010 +0200
     2.3 @@ -11,7 +11,8 @@
     2.4    val show_types: bool Unsynchronized.ref
     2.5    val show_free_types: bool Config.T
     2.6    val show_all_types: bool Config.T
     2.7 -  val show_structs: bool Unsynchronized.ref
     2.8 +  val show_structs_value: Config.value Config.T
     2.9 +  val show_structs: bool Config.T
    2.10    val show_question_marks_default: bool Unsynchronized.ref
    2.11    val show_question_marks_value: Config.value Config.T
    2.12    val show_question_marks: bool Config.T
    2.13 @@ -53,7 +54,9 @@
    2.14  val show_brackets = Unsynchronized.ref false;
    2.15  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    2.16  val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
    2.17 -val show_structs = Unsynchronized.ref false;
    2.18 +
    2.19 +val show_structs_value = Config.declare "show_structs" (fn _ => Config.Bool false);
    2.20 +val show_structs = Config.bool show_structs_value;
    2.21  
    2.22  val show_question_marks_default = Unsynchronized.ref true;
    2.23  val show_question_marks_value =
    2.24 @@ -119,8 +122,9 @@
    2.25  
    2.26  (** term_to_ast **)
    2.27  
    2.28 -fun ast_of_term idents consts ctxt trf show_types show_sorts show_structs tm =
    2.29 +fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
    2.30    let
    2.31 +    val show_structs = Config.get ctxt show_structs;
    2.32      val show_free_types = Config.get ctxt show_free_types;
    2.33      val show_all_types = Config.get ctxt show_all_types;
    2.34  
    2.35 @@ -202,8 +206,7 @@
    2.36  
    2.37  fun term_to_ast idents consts ctxt trf tm =
    2.38    ast_of_term idents consts ctxt trf
    2.39 -    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types)
    2.40 -    (! show_sorts) (! show_structs) tm;
    2.41 +    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types) (! show_sorts) tm;
    2.42  
    2.43  
    2.44  
     3.1 --- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:36:16 2010 +0200
     3.2 +++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:57:21 2010 +0200
     3.3 @@ -446,7 +446,7 @@
     3.4  
     3.5  val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
     3.6  val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
     3.7 -val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
     3.8 +val _ = add_option "show_structs" (Config.put show_structs o boolean);
     3.9  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    3.10  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
    3.11  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);