1.1 --- a/NEWS	Sun Sep 05 19:47:40 2010 +0200
     1.2 +++ b/NEWS	Sun Sep 05 21:41:24 2010 +0200
     1.3 @@ -31,6 +31,8 @@
     1.4    ML (Config.T)                 Isar (attribute)
     1.5  
     1.6    eta_contract                  eta_contract
     1.7 +  show_sorts                    show_sorts
     1.8 +  show_types                    show_types
     1.9    show_question_marks           show_question_marks
    1.10    show_consts                   show_consts
    1.11  

     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 19:47:40 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Sun Sep 05 21:41:24 2010 +0200
     2.3 @@ -96,8 +96,8 @@
     2.4  
     2.5  text {*
     2.6    \begin{mldecls} 
     2.7 -    @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.8 -    @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.9 +    @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
    2.10 +    @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
    2.11      @{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
    2.12      @{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
    2.13      @{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\

     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 19:47:40 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Sun Sep 05 21:41:24 2010 +0200
     3.3 @@ -118,8 +118,8 @@
     3.4  %
     3.5  \begin{isamarkuptext}%
     3.6  \begin{mldecls} 
     3.7 -    \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
     3.8 -    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
     3.9 +    \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
    3.10 +    \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
    3.11      \indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
    3.12      \indexdef{}{ML}{long\_names}\verb|long_names: bool Unsynchronized.ref| & default \verb|false| \\
    3.13      \indexdef{}{ML}{short\_names}\verb|short_names: bool Unsynchronized.ref| & default \verb|false| \\

     4.1 --- a/src/HOL/Groups.thy	Sun Sep 05 19:47:40 2010 +0200
     4.2 +++ b/src/HOL/Groups.thy	Sun Sep 05 21:41:24 2010 +0200
     4.3 @@ -124,11 +124,11 @@
     4.4  simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
     4.5  simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
     4.6  
     4.7 -typed_print_translation {*
     4.8 +typed_print_translation (advanced) {*
     4.9  let
    4.10 -  fun tr' c = (c, fn show_sorts => fn T => fn ts =>
    4.11 -    if (not o null) ts orelse T = dummyT
    4.12 -      orelse not (! show_types) andalso can Term.dest_Type T
    4.13 +  fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
    4.14 +    if not (null ts) orelse T = dummyT
    4.15 +      orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
    4.16      then raise Match
    4.17      else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
    4.18  in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;

     5.1 --- a/src/HOL/Import/proof_kernel.ML	Sun Sep 05 19:47:40 2010 +0200
     5.2 +++ b/src/HOL/Import/proof_kernel.ML	Sun Sep 05 21:41:24 2010 +0200
     5.3 @@ -191,6 +191,7 @@
     5.4      let
     5.5          val ctxt = ctxt0
     5.6            |> Config.put show_all_types true
     5.7 +          |> Config.put show_sorts true
     5.8            |> Config.put Syntax.ambiguity_enabled true;
     5.9          val {t,T,...} = rep_cterm ct
    5.10          (* Hack to avoid parse errors with Trueprop *)
    5.11 @@ -199,8 +200,7 @@
    5.12      in
    5.13          quote (
    5.14          Print_Mode.setmp [] (
    5.15 -        setmp_CRITICAL show_brackets false (
    5.16 -        setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
    5.17 +        setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
    5.18          ct)
    5.19      end
    5.20  
    5.21 @@ -214,7 +214,7 @@
    5.22          val ct  = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
    5.23                     handle TERM _ => ct
    5.24          fun match u = t aconv u
    5.25 -        fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
    5.26 +        fun G 0 f ctxt x = f (Config.put show_types true (Config.put show_sorts true ctxt)) x
    5.27            | G 1 f ctxt x = setmp_CRITICAL show_brackets true (G 0) f ctxt x
    5.28            | G 2 f ctxt x = G 0 f (Config.put show_all_types true ctxt) x
    5.29            | G 3 f ctxt x = setmp_CRITICAL show_brackets true (G 2) f ctxt x

     6.1 --- a/src/HOL/Statespace/state_space.ML	Sun Sep 05 19:47:40 2010 +0200
     6.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Sep 05 21:41:24 2010 +0200
     6.3 @@ -439,8 +439,8 @@
     6.4        in Context.mapping I upd_prf ctxt end;
     6.5  
     6.6     fun string_of_typ T =
     6.7 -      setmp_CRITICAL show_sorts true
     6.8 -       (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
     6.9 +      Print_Mode.setmp []
    6.10 +        (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
    6.11     val fixestate = (case state_type of
    6.12           NONE => []
    6.13         | SOME s =>

     7.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Sep 05 19:47:40 2010 +0200
     7.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Sep 05 21:41:24 2010 +0200
     7.3 @@ -288,7 +288,7 @@
     7.4        Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
     7.5        orelse error (cat_lines
     7.6        ["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
     7.7 -       setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
     7.8 +       Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
     7.9  
    7.10      val _ = map check_sorts fixes
    7.11    in

     8.1 --- a/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Sep 05 19:47:40 2010 +0200
     8.2 +++ b/src/HOL/Tools/Nitpick/nitpick_util.ML	Sun Sep 05 21:41:24 2010 +0200
     8.3 @@ -281,7 +281,8 @@
     8.4  
     8.5  fun set_show_all_types ctxt =
     8.6    Config.put show_all_types
     8.7 -    (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
     8.8 +    (Config.get ctxt show_types orelse Config.get ctxt show_sorts
     8.9 +      orelse Config.get ctxt show_all_types) ctxt
    8.10  
    8.11  val indent_size = 2
    8.12  

     9.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 05 19:47:40 2010 +0200
     9.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML	Sun Sep 05 21:41:24 2010 +0200
     9.3 @@ -947,11 +947,12 @@
     9.4  
     9.5  fun string_for_proof ctxt0 full_types i n =
     9.6    let
     9.7 -    val ctxt = Config.put show_free_types false ctxt0
     9.8 +    val ctxt = ctxt0
     9.9 +      |> Config.put show_free_types false
    9.10 +      |> Config.put show_types true
    9.11      fun fix_print_mode f x =
    9.12 -      setmp_CRITICAL show_types true
    9.13 -           (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    9.14 -                                     (print_mode_value ())) f) x
    9.15 +      Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
    9.16 +                               (print_mode_value ())) f x
    9.17      fun do_indent ind = replicate_string (ind * indent_size) " "
    9.18      fun do_free (s, T) =
    9.19        maybe_quote s ^ " :: " ^

    10.1 --- a/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 19:47:40 2010 +0200
    10.2 +++ b/src/HOL/Tools/numeral_syntax.ML	Sun Sep 05 21:41:24 2010 +0200
    10.3 @@ -69,15 +69,15 @@
    10.4  
    10.5  in
    10.6  
    10.7 -fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
    10.8 +fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
    10.9        let val t' =
   10.10 -        if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
   10.11 +        if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
   10.12          else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
   10.13        in list_comb (t', ts) end
   10.14 -  | numeral_tr' _ (*"number_of"*) T (t :: ts) =
   10.15 +  | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
   10.16        if T = dummyT then list_comb (syntax_numeral t, ts)
   10.17        else raise Match
   10.18 -  | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
   10.19 +  | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
   10.20  
   10.21  end;
   10.22  
   10.23 @@ -86,6 +86,6 @@
   10.24  
   10.25  val setup =
   10.26    Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
   10.27 -  Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
   10.28 +  Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
   10.29  
   10.30  end;

    11.1 --- a/src/HOL/Tools/record.ML	Sun Sep 05 19:47:40 2010 +0200
    11.2 +++ b/src/HOL/Tools/record.ML	Sun Sep 05 21:41:24 2010 +0200
    11.3 @@ -699,9 +699,9 @@
    11.4  
    11.5                      val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
    11.6                        handle Type.TYPE_MATCH => err "type is no proper record (extension)";
    11.7 +                    val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
    11.8                      val alphas' =
    11.9 -                      map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
   11.10 -                        (but_last alphas);
   11.11 +                      map (term_of_typ o Envir.norm_type subst o varifyT) (but_last alphas);
   11.12  
   11.13                      val more' = mk_ext rest;
   11.14                    in
   11.15 @@ -810,7 +810,7 @@
   11.16      val T = decode_type thy t;
   11.17      val varifyT = varifyT (Term.maxidx_of_typ T);
   11.18  
   11.19 -    val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
   11.20 +    val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
   11.21  
   11.22      fun strip_fields T =
   11.23        (case T of
   11.24 @@ -856,7 +856,7 @@
   11.25  
   11.26      fun mk_type_abbr subst name args =
   11.27        let val abbrT = Type (name, map (varifyT o TFree) args)
   11.28 -      in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
   11.29 +      in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
   11.30  
   11.31      fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
   11.32    in

    12.1 --- a/src/HOL/ex/Numeral.thy	Sun Sep 05 19:47:40 2010 +0200
    12.2 +++ b/src/HOL/ex/Numeral.thy	Sun Sep 05 21:41:24 2010 +0200
    12.3 @@ -293,7 +293,7 @@
    12.4  in [(@{syntax_const "_Numerals"}, numeral_tr)] end
    12.5  *}
    12.6  
    12.7 -typed_print_translation {*
    12.8 +typed_print_translation (advanced) {*
    12.9  let
   12.10    fun dig b n = b + 2 * n; 
   12.11    fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
   12.12 @@ -301,14 +301,15 @@
   12.13      | int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
   12.14          dig 1 (int_of_num' n)
   12.15      | int_of_num' (Const (@{const_syntax One}, _)) = 1;
   12.16 -  fun num_tr' show_sorts T [n] =
   12.17 +  fun num_tr' ctxt show_sorts T [n] =
   12.18      let
   12.19        val k = int_of_num' n;
   12.20        val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
   12.21 -    in case T
   12.22 -     of Type (@{type_name fun}, [_, T']) =>
   12.23 -         if not (! show_types) andalso can Term.dest_Type T' then t'
   12.24 -         else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
   12.25 +    in
   12.26 +      case T of
   12.27 +        Type (@{type_name fun}, [_, T']) =>
   12.28 +          if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
   12.29 +          else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
   12.30        | T' => if T' = dummyT then t' else raise Match
   12.31      end;
   12.32  in [(@{const_syntax of_num}, num_tr')] end

    13.1 --- a/src/Pure/Isar/attrib.ML	Sun Sep 05 19:47:40 2010 +0200
    13.2 +++ b/src/Pure/Isar/attrib.ML	Sun Sep 05 21:41:24 2010 +0200
    13.3 @@ -392,7 +392,9 @@
    13.4  (* theory setup *)
    13.5  
    13.6  val _ = Context.>> (Context.map_theory
    13.7 - (register_config Syntax.show_structs_value #>
    13.8 + (register_config Syntax.show_sorts_value #>
    13.9 +  register_config Syntax.show_types_value #>
   13.10 +  register_config Syntax.show_structs_value #>
   13.11    register_config Syntax.show_question_marks_value #>
   13.12    register_config Syntax.ambiguity_level_value #>
   13.13    register_config Syntax.eta_contract_value #>

    14.1 --- a/src/Pure/Isar/class.ML	Sun Sep 05 19:47:40 2010 +0200
    14.2 +++ b/src/Pure/Isar/class.ML	Sun Sep 05 21:41:24 2010 +0200
    14.3 @@ -164,7 +164,7 @@
    14.4          val Ss = Sorts.mg_domain algebra tyco [class];
    14.5        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    14.6      fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
    14.7 -      ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
    14.8 +      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
    14.9      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
   14.10        (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
   14.11        (SOME o Pretty.block) [Pretty.str "supersort: ",

    15.1 --- a/src/Pure/Isar/code.ML	Sun Sep 05 19:47:40 2010 +0200
    15.2 +++ b/src/Pure/Isar/code.ML	Sun Sep 05 21:41:24 2010 +0200
    15.3 @@ -110,7 +110,8 @@
    15.4  
    15.5  (* printing *)
    15.6  
    15.7 -fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
    15.8 +fun string_of_typ thy =
    15.9 +  Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
   15.10  
   15.11  fun string_of_const thy c = case AxClass.inst_of_param thy c
   15.12   of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)

    16.1 --- a/src/Pure/Isar/locale.ML	Sun Sep 05 19:47:40 2010 +0200
    16.2 +++ b/src/Pure/Isar/locale.ML	Sun Sep 05 21:41:24 2010 +0200
    16.3 @@ -180,7 +180,8 @@
    16.4      fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
    16.5      fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
    16.6      val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
    16.7 -    fun prt_term' t = if !show_types
    16.8 +    fun prt_term' t =
    16.9 +      if Config.get ctxt show_types
   16.10        then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
   16.11          Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
   16.12        else prt_term t;

    17.1 --- a/src/Pure/Isar/obtain.ML	Sun Sep 05 19:47:40 2010 +0200
    17.2 +++ b/src/Pure/Isar/obtain.ML	Sun Sep 05 21:41:24 2010 +0200
    17.3 @@ -215,7 +215,7 @@
    17.4      val thy = ProofContext.theory_of ctxt;
    17.5      val certT = Thm.ctyp_of thy;
    17.6      val cert = Thm.cterm_of thy;
    17.7 -    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
    17.8 +    val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
    17.9  
   17.10      fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
   17.11  

    18.1 --- a/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 19:47:40 2010 +0200
    18.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Sun Sep 05 21:41:24 2010 +0200
    18.3 @@ -111,10 +111,10 @@
    18.4  
    18.5  
    18.6  val display_preferences =
    18.7 - [bool_pref show_types
    18.8 + [bool_pref show_types_default
    18.9      "show-types"
   18.10      "Include types in display of Isabelle terms",
   18.11 -  bool_pref show_sorts
   18.12 +  bool_pref show_sorts_default
   18.13      "show-sorts"
   18.14      "Include sorts in display of Isabelle terms",
   18.15    bool_pref show_consts_default

    19.1 --- a/src/Pure/Syntax/printer.ML	Sun Sep 05 19:47:40 2010 +0200
    19.2 +++ b/src/Pure/Syntax/printer.ML	Sun Sep 05 21:41:24 2010 +0200
    19.3 @@ -7,8 +7,12 @@
    19.4  signature PRINTER0 =
    19.5  sig
    19.6    val show_brackets: bool Unsynchronized.ref
    19.7 -  val show_sorts: bool Unsynchronized.ref
    19.8 -  val show_types: bool Unsynchronized.ref
    19.9 +  val show_sorts_default: bool Unsynchronized.ref
   19.10 +  val show_sorts_value: Config.value Config.T
   19.11 +  val show_sorts: bool Config.T
   19.12 +  val show_types_default: bool Unsynchronized.ref
   19.13 +  val show_types_value: Config.value Config.T
   19.14 +  val show_types: bool Config.T
   19.15    val show_free_types: bool Config.T
   19.16    val show_all_types: bool Config.T
   19.17    val show_structs_value: Config.value Config.T
   19.18 @@ -49,8 +53,14 @@
   19.19  
   19.20  (** options for printing **)
   19.21  
   19.22 -val show_types = Unsynchronized.ref false;
   19.23 -val show_sorts = Unsynchronized.ref false;
   19.24 +val show_types_default = Unsynchronized.ref false;
   19.25 +val show_types_value = Config.declare "show_types" (fn _ => Config.Bool (! show_types_default));
   19.26 +val show_types = Config.bool show_types_value;
   19.27 +
   19.28 +val show_sorts_default = Unsynchronized.ref false;
   19.29 +val show_sorts_value = Config.declare "show_sorts" (fn _ => Config.Bool (! show_sorts_default));
   19.30 +val show_sorts = Config.bool show_sorts_value;
   19.31 +
   19.32  val show_brackets = Unsynchronized.ref false;
   19.33  val show_free_types = Config.bool (Config.declare "show_free_types" (fn _ => Config.Bool true));
   19.34  val show_all_types = Config.bool (Config.declare "show_all_types" (fn _ => Config.Bool false));
   19.35 @@ -78,7 +88,7 @@
   19.36        | app_first (f :: fs) = f ctxt args handle Match => app_first fs;
   19.37    in app_first fns end;
   19.38  
   19.39 -fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
   19.40 +fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
   19.41  
   19.42  
   19.43  (* simple_ast_of *)
   19.44 @@ -102,6 +112,7 @@
   19.45  
   19.46  fun ast_of_termT ctxt trf tm =
   19.47    let
   19.48 +    val ctxt' = Config.put show_sorts false ctxt;
   19.49      fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
   19.50        | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
   19.51        | ast_of (Const (a, _)) = trans a []
   19.52 @@ -111,19 +122,24 @@
   19.53            | (f, args) => Ast.Appl (map ast_of (f :: args)))
   19.54        | ast_of t = simple_ast_of ctxt t
   19.55      and trans a args =
   19.56 -      ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
   19.57 +      ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
   19.58          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
   19.59    in ast_of tm end;
   19.60  
   19.61  fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
   19.62 -fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
   19.63 +fun typ_to_ast ctxt trf T =
   19.64 +  ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
   19.65  
   19.66  
   19.67  
   19.68  (** term_to_ast **)
   19.69  
   19.70 -fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
   19.71 +fun term_to_ast idents consts ctxt trf tm =
   19.72    let
   19.73 +    val show_types =
   19.74 +      Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
   19.75 +      Config.get ctxt show_all_types;
   19.76 +    val show_sorts = Config.get ctxt show_sorts;
   19.77      val show_structs = Config.get ctxt show_structs;
   19.78      val show_free_types = Config.get ctxt show_free_types;
   19.79      val show_all_types = Config.get ctxt show_all_types;
   19.80 @@ -188,7 +204,7 @@
   19.81        | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
   19.82  
   19.83      and trans a T args =
   19.84 -      ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
   19.85 +      ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
   19.86          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
   19.87  
   19.88      and constrain t T =
   19.89 @@ -204,10 +220,6 @@
   19.90      |> ast_of
   19.91    end;
   19.92  
   19.93 -fun term_to_ast idents consts ctxt trf tm =
   19.94 -  ast_of_term idents consts ctxt trf
   19.95 -    (! show_types orelse ! show_sorts orelse Config.get ctxt show_all_types) (! show_sorts) tm;
   19.96 -
   19.97  
   19.98  
   19.99  (** type prtabs **)

    20.1 --- a/src/Pure/Thy/thy_output.ML	Sun Sep 05 19:47:40 2010 +0200
    20.2 +++ b/src/Pure/Thy/thy_output.ML	Sun Sep 05 21:41:24 2010 +0200
    20.3 @@ -444,8 +444,8 @@
    20.4  
    20.5  (* options *)
    20.6  
    20.7 -val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
    20.8 -val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
    20.9 +val _ = add_option "show_types" (Config.put show_types o boolean);
   20.10 +val _ = add_option "show_sorts" (Config.put show_sorts o boolean);
   20.11  val _ = add_option "show_structs" (Config.put show_structs o boolean);
   20.12  val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
   20.13  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);

    21.1 --- a/src/Pure/axclass.ML	Sun Sep 05 19:47:40 2010 +0200
    21.2 +++ b/src/Pure/axclass.ML	Sun Sep 05 21:41:24 2010 +0200
    21.3 @@ -519,7 +519,7 @@
    21.4      fun check_constraint (a, S) =
    21.5        if Sign.subsort thy (super, S) then ()
    21.6        else error ("Sort constraint of type variable " ^
    21.7 -        setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
    21.8 +        Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^
    21.9          " needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
   21.10  
   21.11  

    22.1 --- a/src/Pure/goal_display.ML	Sun Sep 05 19:47:40 2010 +0200
    22.2 +++ b/src/Pure/goal_display.ML	Sun Sep 05 21:41:24 2010 +0200
    22.3 @@ -77,12 +77,20 @@
    22.4  
    22.5  fun pretty_goals ctxt0 state =
    22.6    let
    22.7 -    val ctxt = Config.put show_free_types false ctxt0;
    22.8 +    val ctxt = ctxt0
    22.9 +      |> Config.put show_free_types false
   22.10 +      |> Config.put show_types
   22.11 +       (Config.get ctxt0 show_types orelse
   22.12 +        Config.get ctxt0 show_sorts orelse
   22.13 +        Config.get ctxt0 show_all_types)
   22.14 +      |> Config.put show_sorts false;
   22.15  
   22.16 -    val show_all_types = Config.get ctxt show_all_types;
   22.17 +    val show_sorts0 = Config.get ctxt0 show_sorts;
   22.18 +    val show_types = Config.get ctxt show_types;
   22.19 +    val show_consts = Config.get ctxt show_consts
   22.20 +    val show_main_goal = Config.get ctxt show_main_goal;
   22.21      val goals_limit = Config.get ctxt goals_limit;
   22.22      val goals_total = Config.get ctxt goals_total;
   22.23 -    val show_main_goal = Config.get ctxt show_main_goal;
   22.24  
   22.25      val prt_sort = Syntax.pretty_sort ctxt;
   22.26      val prt_typ = Syntax.pretty_typ ctxt;
   22.27 @@ -120,23 +128,18 @@
   22.28      val {prop, tpairs, ...} = Thm.rep_thm state;
   22.29      val (As, B) = Logic.strip_horn prop;
   22.30      val ngoals = length As;
   22.31 -
   22.32 -    fun pretty_gs (types, sorts) =
   22.33 -      (if show_main_goal then [prt_term B] else []) @
   22.34 -       (if ngoals = 0 then [Pretty.str "No subgoals!"]
   22.35 -        else if ngoals > goals_limit then
   22.36 -          pretty_subgoals (take goals_limit As) @
   22.37 -          (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   22.38 -           else [])
   22.39 -        else pretty_subgoals As) @
   22.40 -      pretty_ffpairs tpairs @
   22.41 -      (if Config.get ctxt show_consts then pretty_consts prop else []) @
   22.42 -      (if types then pretty_vars prop else []) @
   22.43 -      (if sorts then pretty_varsT prop else []);
   22.44    in
   22.45 -    setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
   22.46 -      (setmp_CRITICAL show_sorts false pretty_gs)
   22.47 -   (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
   22.48 +    (if show_main_goal then [prt_term B] else []) @
   22.49 +     (if ngoals = 0 then [Pretty.str "No subgoals!"]
   22.50 +      else if ngoals > goals_limit then
   22.51 +        pretty_subgoals (take goals_limit As) @
   22.52 +        (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
   22.53 +         else [])
   22.54 +      else pretty_subgoals As) @
   22.55 +    pretty_ffpairs tpairs @
   22.56 +    (if show_consts then pretty_consts prop else []) @
   22.57 +    (if show_types then pretty_vars prop else []) @
   22.58 +    (if show_sorts0 then pretty_varsT prop else [])
   22.59    end;
   22.60  
   22.61  fun pretty_goals_without_context th =

    23.1 --- a/src/Pure/theory.ML	Sun Sep 05 19:47:40 2010 +0200
    23.2 +++ b/src/Pure/theory.ML	Sun Sep 05 21:41:24 2010 +0200
    23.3 @@ -161,11 +161,13 @@
    23.4          | TERM (msg, _) => error msg;
    23.5      val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    23.6  
    23.7 +    val ctxt = Syntax.init_pretty_global thy
    23.8 +      |> Config.put show_sorts true;
    23.9      val bad_sorts =
   23.10        rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
   23.11      val _ = null bad_sorts orelse
   23.12        error ("Illegal sort constraints in primitive specification: " ^
   23.13 -        commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
   23.14 +        commas (map (Syntax.string_of_typ ctxt) bad_sorts));
   23.15    in
   23.16      (b, Sign.no_vars (Syntax.init_pretty_global thy) t)
   23.17    end handle ERROR msg =>
   23.18 @@ -217,18 +219,18 @@
   23.19        handle TYPE (msg, _, _) => error msg;
   23.20      val T' = Logic.varifyT_global T;
   23.21  
   23.22 -    fun message txt =
   23.23 +    val ctxt = Syntax.init_pretty_global thy;
   23.24 +    fun message sorts txt =
   23.25        [Pretty.block [Pretty.str "Specification of constant ",
   23.26 -        Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
   23.27 +        Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   23.28 +        Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
   23.29          Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
   23.30    in
   23.31      if Sign.typ_instance thy (declT, T') then ()
   23.32      else if Type.raw_instance (declT, T') then
   23.33 -      error (setmp_CRITICAL show_sorts true
   23.34 -        message "imposes additional sort constraints on the constant declaration")
   23.35 +      error (message true "imposes additional sort constraints on the constant declaration")
   23.36      else if overloaded then ()
   23.37 -    else warning (message "is strictly less general than the declared type");
   23.38 -    (c, T)
   23.39 +    else warning (message false "is strictly less general than the declared type")
   23.40    end;
   23.41  
   23.42  
   23.43 @@ -272,7 +274,7 @@
   23.44        | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
   23.45        | const_of _ = error "Attempt to finalize non-constant term";
   23.46      fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
   23.47 -    val finalize = specify o check_overloading thy overloaded o const_of o
   23.48 +    val finalize = specify o tap (check_overloading thy overloaded) o const_of o
   23.49        Sign.cert_term thy o prep_term thy;
   23.50    in thy |> map_defs (fold finalize args) end;
   23.51  

    24.1 --- a/src/Tools/nbe.ML	Sun Sep 05 19:47:40 2010 +0200
    24.2 +++ b/src/Tools/nbe.ML	Sun Sep 05 21:41:24 2010 +0200
    24.3 @@ -552,10 +552,11 @@
    24.4        singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
    24.5          (try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
    24.6        (Type_Infer.constrain ty' t);
    24.7 -    fun check_tvars t = if null (Term.add_tvars t []) then t else
    24.8 -      error ("Illegal schematic type variables in normalized term: "
    24.9 -        ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
   24.10 -    val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
   24.11 +    val string_of_term =
   24.12 +      Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
   24.13 +    fun check_tvars t =
   24.14 +      if null (Term.add_tvars t []) then t
   24.15 +      else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
   24.16    in
   24.17      compile_eval thy program (vs, t) deps
   24.18      |> traced (fn t => "Normalized:\n" ^ string_of_term t)