# HG changeset patch
# User wenzelm
# Date 1283547441 -7200
# Node ID e7ecbe86d22e70b23abc4c112339971421f14adf
# Parent  ee117c5b3b758480b44e1b3ebda2304c0061063d
turned show_structs into proper configuration option;

diff -r ee117c5b3b75 -r e7ecbe86d22e src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Sep 03 22:36:16 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Sep 03 22:57:21 2010 +0200
@@ -392,7 +392,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_question_marks_value #>
+ (register_config Syntax.show_structs_value #>
+  register_config Syntax.show_question_marks_value #>
   register_config Syntax.ambiguity_level_value #>
   register_config Goal_Display.goals_limit_value #>
   register_config Goal_Display.show_main_goal_value #>
diff -r ee117c5b3b75 -r e7ecbe86d22e src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Fri Sep 03 22:36:16 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Fri Sep 03 22:57:21 2010 +0200
@@ -11,7 +11,8 @@
   val show_types: bool Unsynchronized.ref
   val show_free_types: bool Config.T
   val show_all_types: bool Config.T
-  val show_structs: bool Unsynchronized.ref
+  val show_structs_value: Config.value Config.T
+  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: bool Config.T
@@ -53,7 +54,9 @@
 val show_brackets = Unsynchronized.ref false;
 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 = Unsynchronized.ref false;
+
+val show_structs_value = Config.declare "show_structs" (fn _ => Config.Bool false);
+val show_structs = Config.bool show_structs_value;
 
 val show_question_marks_default = Unsynchronized.ref true;
 val show_question_marks_value =
@@ -119,8 +122,9 @@
 
 (** term_to_ast **)
 
-fun ast_of_term idents consts ctxt trf show_types show_sorts show_structs tm =
+fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
   let
+    val show_structs = Config.get ctxt show_structs;
     val show_free_types = Config.get ctxt show_free_types;
     val show_all_types = Config.get ctxt show_all_types;
 
@@ -202,8 +206,7 @@
 
 fun term_to_ast idents consts ctxt trf tm =
   ast_of_term idents consts ctxt trf
-    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types)
-    (! show_sorts) (! show_structs) tm;
+    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types) (! show_sorts) tm;
 
 
 
diff -r ee117c5b3b75 -r e7ecbe86d22e src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:36:16 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Sep 03 22:57:21 2010 +0200
@@ -446,7 +446,7 @@
 
 val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
 val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
-val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
+val _ = add_option "show_structs" (Config.put show_structs o boolean);
 val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
 val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
 val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);