# HG changeset patch
# User wenzelm
# Date 1283721381 -7200
# Node ID ccb53edd59f0fd78f91a5b786f261081d26b3807
# Parent  b0b3b6318e3bd7a074daa56457d6ede88a2196a1
turned show_brackets into proper configuration option;
Sign.certify/type_check: dropped Syntax.pp_show_brackets, which is hard to hold up due to Pretty.pp and not even present in the regular end-user type check;

diff -r b0b3b6318e3b -r ccb53edd59f0 NEWS
--- a/NEWS	Sun Sep 05 22:23:48 2010 +0200
+++ b/NEWS	Sun Sep 05 23:16:21 2010 +0200
@@ -31,6 +31,7 @@
   ML (Config.T)                 Isar (attribute)
 
   eta_contract                  eta_contract
+  show_brackets                 show_brackets
   show_sorts                    show_sorts
   show_types                    show_types
   show_question_marks           show_question_marks
diff -r b0b3b6318e3b -r ccb53edd59f0 doc-src/IsarRef/Thy/Inner_Syntax.thy
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 22:23:48 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 23:16:21 2010 +0200
@@ -102,7 +102,7 @@
     @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
-    @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
+    @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
     @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
     @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
     @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
diff -r b0b3b6318e3b -r ccb53edd59f0 doc-src/IsarRef/Thy/document/Inner_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 22:23:48 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 23:16:21 2010 +0200
@@ -124,7 +124,7 @@
     \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
     \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
-    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
+    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
     \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
     \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
     \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
diff -r b0b3b6318e3b -r ccb53edd59f0 src/HOL/Import/proof_kernel.ML
--- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -190,6 +190,7 @@
 fun simple_smart_string_of_cterm ctxt0 ct =
     let
         val ctxt = ctxt0
+          |> Config.put show_brackets false
           |> Config.put show_all_types true
           |> Config.put show_sorts true
           |> Config.put Syntax.ambiguity_enabled true;
@@ -198,10 +199,7 @@
         val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
                            handle TERM _ => ct
     in
-        quote (
-        Print_Mode.setmp [] (
-        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
-        ct)
+        quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
     end
 
 exception SMART_STRING
@@ -215,14 +213,14 @@
                    handle TERM _ => ct
         fun match u = t aconv u
         fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
-          | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
+          | G 1 f ctxt x = G 0 f (Config.put show_brackets true ctxt) x
           | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
-          | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
+          | G 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
           | G _ _ _ _ = raise SMART_STRING
         fun F n =
             let
                 val str =
-                  setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
+                  G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
                 val u = Syntax.parse_term ctxt str
                   |> Type_Infer.constrain T |> Syntax.check_term ctxt
             in
diff -r b0b3b6318e3b -r ccb53edd59f0 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/Isar/attrib.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -392,7 +392,8 @@
 (* theory setup *)
 
 val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_sorts_value #>
+ (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 #>
diff -r b0b3b6318e3b -r ccb53edd59f0 src/Pure/ProofGeneral/preferences.ML
--- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -123,7 +123,7 @@
   bool_pref long_names
     "long-names"
     "Show fully qualified names in Isabelle terms",
-  bool_pref show_brackets
+  bool_pref show_brackets_default
     "show-brackets"
     "Show full bracketing in Isabelle terms",
   bool_pref Goal_Display.show_main_goal_default
diff -r b0b3b6318e3b -r ccb53edd59f0 src/Pure/Syntax/printer.ML
--- a/src/Pure/Syntax/printer.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/Syntax/printer.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -6,13 +6,15 @@
 
 signature PRINTER0 =
 sig
-  val show_brackets: bool Unsynchronized.ref
+  val show_brackets_default: bool Unsynchronized.ref
+  val show_brackets_value: Config.value Config.T
+  val show_brackets: bool Config.T
+  val show_types_default: bool Unsynchronized.ref
+  val show_types_value: Config.value Config.T
+  val show_types: bool Config.T
   val show_sorts_default: bool Unsynchronized.ref
   val show_sorts_value: Config.value Config.T
   val show_sorts: bool Config.T
-  val show_types_default: bool Unsynchronized.ref
-  val show_types_value: Config.value Config.T
-  val show_types: 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
@@ -20,7 +22,6 @@
   val show_question_marks_default: bool Unsynchronized.ref
   val show_question_marks_value: Config.value Config.T
   val show_question_marks: bool Config.T
-  val pp_show_brackets: Pretty.pp -> Pretty.pp
 end;
 
 signature PRINTER =
@@ -53,6 +54,11 @@
 
 (** options for printing **)
 
+val show_brackets_default = Unsynchronized.ref false;
+val show_brackets_value =
+  Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
+val show_brackets = Config.bool show_brackets_value;
+
 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;
@@ -61,7 +67,6 @@
 val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
 val show_sorts = Config.bool show_sorts_value;
 
-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));
 
@@ -73,9 +78,6 @@
   Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
 val show_question_marks = Config.bool show_question_marks_value;
 
-fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
-  Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
-
 
 
 (** misc utils **)
@@ -315,6 +317,7 @@
 fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
   let
     val {extern_class, extern_type, extern_const} = extern;
+    val show_brackets = Config.get ctxt show_brackets;
 
     fun token_trans a x =
       (case tokentrf a of
@@ -361,8 +364,7 @@
           in (T :: Ts, args') end
 
     and parT markup (pr, args, p, p': int) = #1 (synT markup
-          (if p > p' orelse
-            (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
+          (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
             then [Block (1, Space "(" :: pr @ [Space ")"])]
             else pr, args))
 
diff -r b0b3b6318e3b -r ccb53edd59f0 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/Syntax/syntax.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -760,7 +760,7 @@
         val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
         val len = length results;
 
-        val show_term = setmp_CRITICAL Printer.show_brackets true (string_of_term ctxt);
+        val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
       in
         if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
         else if len = 1 then
diff -r b0b3b6318e3b -r ccb53edd59f0 src/Pure/sign.ML
--- a/src/Pure/sign.ML	Sun Sep 05 22:23:48 2010 +0200
+++ b/src/Pure/sign.ML	Sun Sep 05 23:16:21 2010 +0200
@@ -270,8 +270,7 @@
         val xs = map Free bs;           (*we do not rename here*)
         val t' = subst_bounds (xs, t);
         val u' = subst_bounds (xs, u);
-        val msg = cat_lines
-          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
+        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
       in raise TYPE (msg, [T, U], [t', u']) end;
 
     fun typ_of (_, Const (_, T)) = T