turned show_brackets into proper configuration option;
authorwenzelm
Sun Sep 05 23:16:21 2010 +0200 (2010-09-05)
changeset 39137ccb53edd59f0
parent 39136 b0b3b6318e3b
child 39138 53886463f559
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;
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
src/HOL/Import/proof_kernel.ML
src/Pure/Isar/attrib.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Syntax/printer.ML
src/Pure/Syntax/syntax.ML
src/Pure/sign.ML
     1.1 --- a/NEWS	Sun Sep 05 22:23:48 2010 +0200
     1.2 +++ b/NEWS	Sun Sep 05 23:16:21 2010 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    ML (Config.T)                 Isar (attribute)
     1.5  
     1.6    eta_contract                  eta_contract
     1.7 +  show_brackets                 show_brackets
     1.8    show_sorts                    show_sorts
     1.9    show_types                    show_types
    1.10    show_question_marks           show_question_marks
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 22:23:48 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 23:16:21 2010 +0200
     2.3 @@ -102,7 +102,7 @@
     2.4      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.5      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.6      @{index_ML unique_names: "bool Unsynchronized.ref"} & default @{ML true} \\
     2.7 -    @{index_ML show_brackets: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.8 +    @{index_ML show_brackets: "bool Config.T"} & default @{ML false} \\
     2.9      @{index_ML eta_contract: "bool Config.T"} & default @{ML true} \\
    2.10      @{index_ML Goal_Display.goals_limit: "int Config.T"} & default @{ML 10} \\
    2.11      @{index_ML Goal_Display.show_main_goal: "bool Config.T"} & default @{ML false} \\
     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 22:23:48 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 23:16:21 2010 +0200
     3.3 @@ -124,7 +124,7 @@
     3.4      \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
     3.5      \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\
     3.6      \indexdef{}{ML}{unique\_names}\verb|unique_names: bool Unsynchronized.ref| & default \verb|true| \\
     3.7 -    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Unsynchronized.ref| & default \verb|false| \\
     3.8 +    \indexdef{}{ML}{show\_brackets}\verb|show_brackets: bool Config.T| & default \verb|false| \\
     3.9      \indexdef{}{ML}{eta\_contract}\verb|eta_contract: bool Config.T| & default \verb|true| \\
    3.10      \indexdef{}{ML}{Goal\_Display.goals\_limit}\verb|Goal_Display.goals_limit: int Config.T| & default \verb|10| \\
    3.11      \indexdef{}{ML}{Goal\_Display.show\_main\_goal}\verb|Goal_Display.show_main_goal: bool Config.T| & default \verb|false| \\
     4.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 22:23:48 2010 +0200
     4.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 23:16:21 2010 +0200
     4.3 @@ -190,6 +190,7 @@
     4.4  fun simple_smart_string_of_cterm ctxt0 ct =
     4.5      let
     4.6          val ctxt = ctxt0
     4.7 +          |> Config.put show_brackets false
     4.8            |> Config.put show_all_types true
     4.9            |> Config.put show_sorts true
    4.10            |> Config.put Syntax.ambiguity_enabled true;
    4.11 @@ -198,10 +199,7 @@
    4.12          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    4.13                             handle TERM _ => ct
    4.14      in
    4.15 -        quote (
    4.16 -        Print_Mode.setmp [] (
    4.17 -        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
    4.18 -        ct)
    4.19 +        quote (Print_Mode.setmp [] (Syntax.string_of_term ctxt o Thm.term_of) ct)
    4.20      end
    4.21  
    4.22  exception SMART_STRING
    4.23 @@ -215,14 +213,14 @@
    4.24                     handle TERM _ => ct
    4.25          fun match u = t aconv u
    4.26          fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
    4.27 -          | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
    4.28 +          | G 1 f ctxt x = G 0 f (Config.put show_brackets true ctxt) x
    4.29            | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
    4.30 -          | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x
    4.31 +          | G 3 f ctxt x = G 2 f (Config.put show_brackets true ctxt) x
    4.32            | G _ _ _ _ = raise SMART_STRING
    4.33          fun F n =
    4.34              let
    4.35                  val str =
    4.36 -                  setmp_CRITICAL show_brackets false (G n Syntax.string_of_term ctxt) (term_of ct)
    4.37 +                  G n Syntax.string_of_term (Config.put show_brackets false ctxt) (term_of ct)
    4.38                  val u = Syntax.parse_term ctxt str
    4.39                    |> Type_Infer.constrain T |> Syntax.check_term ctxt
    4.40              in
     5.1 --- a/src/Pure/Isar/attrib.ML	Sun Sep 05 22:23:48 2010 +0200
     5.2 +++ b/src/Pure/Isar/attrib.ML	Sun Sep 05 23:16:21 2010 +0200
     5.3 @@ -392,7 +392,8 @@
     5.4  (* theory setup *)
     5.5  
     5.6  val _ = Context.>> (Context.map_theory
     5.7 - (register_config Syntax.show_sorts_value #>
     5.8 + (register_config Syntax.show_brackets_value #>
     5.9 +  register_config Syntax.show_sorts_value #>
    5.10    register_config Syntax.show_types_value #>
    5.11    register_config Syntax.show_structs_value #>
    5.12    register_config Syntax.show_question_marks_value #>
     6.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 22:23:48 2010 +0200
     6.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 23:16:21 2010 +0200
     6.3 @@ -123,7 +123,7 @@
     6.4    bool_pref long_names
     6.5      "long-names"
     6.6      "Show fully qualified names in Isabelle terms",
     6.7 -  bool_pref show_brackets
     6.8 +  bool_pref show_brackets_default
     6.9      "show-brackets"
    6.10      "Show full bracketing in Isabelle terms",
    6.11    bool_pref Goal_Display.show_main_goal_default
     7.1 --- a/src/Pure/Syntax/printer.ML	Sun Sep 05 22:23:48 2010 +0200
     7.2 +++ b/src/Pure/Syntax/printer.ML	Sun Sep 05 23:16:21 2010 +0200
     7.3 @@ -6,13 +6,15 @@
     7.4  
     7.5  signature PRINTER0 =
     7.6  sig
     7.7 -  val show_brackets: bool Unsynchronized.ref
     7.8 +  val show_brackets_default: bool Unsynchronized.ref
     7.9 +  val show_brackets_value: Config.value Config.T
    7.10 +  val show_brackets: bool Config.T
    7.11 +  val show_types_default: bool Unsynchronized.ref
    7.12 +  val show_types_value: Config.value Config.T
    7.13 +  val show_types: bool Config.T
    7.14    val show_sorts_default: bool Unsynchronized.ref
    7.15    val show_sorts_value: Config.value Config.T
    7.16    val show_sorts: bool Config.T
    7.17 -  val show_types_default: bool Unsynchronized.ref
    7.18 -  val show_types_value: Config.value Config.T
    7.19 -  val show_types: bool Config.T
    7.20    val show_free_types: bool Config.T
    7.21    val show_all_types: bool Config.T
    7.22    val show_structs_value: Config.value Config.T
    7.23 @@ -20,7 +22,6 @@
    7.24    val show_question_marks_default: bool Unsynchronized.ref
    7.25    val show_question_marks_value: Config.value Config.T
    7.26    val show_question_marks: bool Config.T
    7.27 -  val pp_show_brackets: Pretty.pp -> Pretty.pp
    7.28  end;
    7.29  
    7.30  signature PRINTER =
    7.31 @@ -53,6 +54,11 @@
    7.32  
    7.33  (** options for printing **)
    7.34  
    7.35 +val show_brackets_default = Unsynchronized.ref false;
    7.36 +val show_brackets_value =
    7.37 +  Config.declare "show_brackets" (fn _ => Config.Bool (! show_brackets_default));
    7.38 +val show_brackets = Config.bool show_brackets_value;
    7.39 +
    7.40  val show_types_default = Unsynchronized.ref false;
    7.41  val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
    7.42  val show_types = Config.bool show_types_value;
    7.43 @@ -61,7 +67,6 @@
    7.44  val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
    7.45  val show_sorts = Config.bool show_sorts_value;
    7.46  
    7.47 -val show_brackets = Unsynchronized.ref false;
    7.48  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
    7.49  val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
    7.50  
    7.51 @@ -73,9 +78,6 @@
    7.52    Config.declare "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    7.53  val show_question_marks = Config.bool show_question_marks_value;
    7.54  
    7.55 -fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
    7.56 -  Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
    7.57 -
    7.58  
    7.59  
    7.60  (** misc utils **)
    7.61 @@ -315,6 +317,7 @@
    7.62  fun pretty extern ctxt tabs trf tokentrf type_mode curried ast0 p0 =
    7.63    let
    7.64      val {extern_class, extern_type, extern_const} = extern;
    7.65 +    val show_brackets = Config.get ctxt show_brackets;
    7.66  
    7.67      fun token_trans a x =
    7.68        (case tokentrf a of
    7.69 @@ -361,8 +364,7 @@
    7.70            in (T :: Ts, args') end
    7.71  
    7.72      and parT markup (pr, args, p, p': int) = #1 (synT markup
    7.73 -          (if p > p' orelse
    7.74 -            (! show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
    7.75 +          (if p > p' orelse (show_brackets andalso p' <> Syn_Ext.max_pri andalso not (is_chain pr))
    7.76              then [Block (1, Space "(" :: pr @ [Space ")"])]
    7.77              else pr, args))
    7.78  
     8.1 --- a/src/Pure/Syntax/syntax.ML	Sun Sep 05 22:23:48 2010 +0200
     8.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Sep 05 23:16:21 2010 +0200
     8.3 @@ -760,7 +760,7 @@
     8.4          val results = map_filter (fn (t, NONE) => SOME t | _ => NONE) (ts ~~ errs);
     8.5          val len = length results;
     8.6  
     8.7 -        val show_term = setmp_CRITICAL Printer.show_brackets true (string_of_term ctxt);
     8.8 +        val show_term = string_of_term (Config.put Printer.show_brackets true ctxt);
     8.9        in
    8.10          if null results then cat_error (ambig_msg ()) (cat_lines (map_filter I errs))
    8.11          else if len = 1 then
     9.1 --- a/src/Pure/sign.ML	Sun Sep 05 22:23:48 2010 +0200
     9.2 +++ b/src/Pure/sign.ML	Sun Sep 05 23:16:21 2010 +0200
     9.3 @@ -270,8 +270,7 @@
     9.4          val xs = map Free bs;           (*we do not rename here*)
     9.5          val t' = subst_bounds (xs, t);
     9.6          val u' = subst_bounds (xs, u);
     9.7 -        val msg = cat_lines
     9.8 -          (Type_Infer.appl_error (Syntax.pp_show_brackets pp) why t' T u' U);
     9.9 +        val msg = cat_lines (Type_Infer.appl_error pp why t' T u' U);
    9.10        in raise TYPE (msg, [T, U], [t', u']) end;
    9.11  
    9.12      fun typ_of (_, Const (_, T)) = T