--- a/NEWS Sun Sep 05 19:47:40 2010 +0200
+++ b/NEWS Sun Sep 05 21:41:24 2010 +0200
@@ -31,6 +31,8 @@
ML (Config.T) Isar (attribute)
eta_contract eta_contract
+ show_sorts show_sorts
+ show_types show_types
show_question_marks show_question_marks
show_consts show_consts
--- a/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Sep 05 19:47:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy Sun Sep 05 21:41:24 2010 +0200
@@ -96,8 +96,8 @@
text {*
\begin{mldecls}
- @{index_ML show_types: "bool Unsynchronized.ref"} & default @{ML false} \\
- @{index_ML show_sorts: "bool Unsynchronized.ref"} & default @{ML false} \\
+ @{index_ML show_types: "bool Config.T"} & default @{ML false} \\
+ @{index_ML show_sorts: "bool Config.T"} & default @{ML false} \\
@{index_ML show_consts: "bool Config.T"} & default @{ML false} \\
@{index_ML long_names: "bool Unsynchronized.ref"} & default @{ML false} \\
@{index_ML short_names: "bool Unsynchronized.ref"} & default @{ML false} \\
--- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Sep 05 19:47:40 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex Sun Sep 05 21:41:24 2010 +0200
@@ -118,8 +118,8 @@
%
\begin{isamarkuptext}%
\begin{mldecls}
- \indexdef{}{ML}{show\_types}\verb|show_types: bool Unsynchronized.ref| & default \verb|false| \\
- \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Unsynchronized.ref| & default \verb|false| \\
+ \indexdef{}{ML}{show\_types}\verb|show_types: bool Config.T| & default \verb|false| \\
+ \indexdef{}{ML}{show\_sorts}\verb|show_sorts: bool Config.T| & default \verb|false| \\
\indexdef{}{ML}{show\_consts}\verb|show_consts: bool Config.T| & default \verb|false| \\
\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| \\
--- a/src/HOL/Groups.thy Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Groups.thy Sun Sep 05 21:41:24 2010 +0200
@@ -124,11 +124,11 @@
simproc_setup reorient_zero ("0 = x") = Reorient_Proc.proc
simproc_setup reorient_one ("1 = x") = Reorient_Proc.proc
-typed_print_translation {*
+typed_print_translation (advanced) {*
let
- fun tr' c = (c, fn show_sorts => fn T => fn ts =>
- if (not o null) ts orelse T = dummyT
- orelse not (! show_types) andalso can Term.dest_Type T
+ fun tr' c = (c, fn ctxt => fn show_sorts => fn T => fn ts =>
+ if not (null ts) orelse T = dummyT
+ orelse not (Config.get ctxt show_types) andalso can Term.dest_Type T
then raise Match
else Syntax.const Syntax.constrainC $ Syntax.const c $ Syntax.term_of_typ show_sorts T);
in map tr' [@{const_syntax Groups.one}, @{const_syntax Groups.zero}] end;
--- a/src/HOL/Import/proof_kernel.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Import/proof_kernel.ML Sun Sep 05 21:41:24 2010 +0200
@@ -191,6 +191,7 @@
let
val ctxt = ctxt0
|> Config.put show_all_types true
+ |> Config.put show_sorts true
|> Config.put Syntax.ambiguity_enabled true;
val {t,T,...} = rep_cterm ct
(* Hack to avoid parse errors with Trueprop *)
@@ -199,8 +200,7 @@
in
quote (
Print_Mode.setmp [] (
- setmp_CRITICAL show_brackets false (
- setmp_CRITICAL show_sorts true (Syntax.string_of_term ctxt o Thm.term_of)))
+ setmp_CRITICAL show_brackets false (Syntax.string_of_term ctxt o Thm.term_of))
ct)
end
@@ -214,7 +214,7 @@
val ct = cterm_of (Thm.theory_of_cterm ct) (HOLogic.dest_Trueprop t)
handle TERM _ => ct
fun match u = t aconv u
- fun G 0 f ctxt x = setmp_CRITICAL show_types true (setmp_CRITICAL show_sorts true) (f ctxt) x
+ 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 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
--- a/src/HOL/Statespace/state_space.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Statespace/state_space.ML Sun Sep 05 21:41:24 2010 +0200
@@ -439,8 +439,8 @@
in Context.mapping I upd_prf ctxt end;
fun string_of_typ T =
- setmp_CRITICAL show_sorts true
- (Print_Mode.setmp [] (Syntax.string_of_typ (ProofContext.init_global thy))) T;
+ Print_Mode.setmp []
+ (Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy))) T;
val fixestate = (case state_type of
NONE => []
| SOME s =>
--- a/src/HOL/Tools/Function/function_common.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Function/function_common.ML Sun Sep 05 21:41:24 2010 +0200
@@ -288,7 +288,7 @@
Sorts.of_sort (Sign.classes_of (ProofContext.theory_of ctxt)) (fT, HOLogic.typeS)
orelse error (cat_lines
["Type of " ^ quote fname ^ " is not of sort " ^ quote "type" ^ ":",
- setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) fT])
+ Syntax.string_of_typ (Config.put show_sorts true ctxt) fT])
val _ = map check_sorts fixes
in
--- a/src/HOL/Tools/Nitpick/nitpick_util.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Nitpick/nitpick_util.ML Sun Sep 05 21:41:24 2010 +0200
@@ -281,7 +281,8 @@
fun set_show_all_types ctxt =
Config.put show_all_types
- (!show_types orelse !show_sorts orelse Config.get ctxt show_all_types) ctxt
+ (Config.get ctxt show_types orelse Config.get ctxt show_sorts
+ orelse Config.get ctxt show_all_types) ctxt
val indent_size = 2
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_reconstruct.ML Sun Sep 05 21:41:24 2010 +0200
@@ -947,11 +947,12 @@
fun string_for_proof ctxt0 full_types i n =
let
- val ctxt = Config.put show_free_types false ctxt0
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types true
fun fix_print_mode f x =
- setmp_CRITICAL show_types true
- (Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
- (print_mode_value ())) f) x
+ Print_Mode.setmp (filter (curry (op =) Symbol.xsymbolsN)
+ (print_mode_value ())) f x
fun do_indent ind = replicate_string (ind * indent_size) " "
fun do_free (s, T) =
maybe_quote s ^ " :: " ^
--- a/src/HOL/Tools/numeral_syntax.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/numeral_syntax.ML Sun Sep 05 21:41:24 2010 +0200
@@ -69,15 +69,15 @@
in
-fun numeral_tr' show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
+fun numeral_tr' ctxt show_sorts (*"number_of"*) (Type (@{type_name fun}, [_, T])) (t :: ts) =
let val t' =
- if not (! show_types) andalso can Term.dest_Type T then syntax_numeral t
+ if not (Config.get ctxt show_types) andalso can Term.dest_Type T then syntax_numeral t
else Syntax.const Syntax.constrainC $ syntax_numeral t $ Syntax.term_of_typ show_sorts T
in list_comb (t', ts) end
- | numeral_tr' _ (*"number_of"*) T (t :: ts) =
+ | numeral_tr' _ _ (*"number_of"*) T (t :: ts) =
if T = dummyT then list_comb (syntax_numeral t, ts)
else raise Match
- | numeral_tr' _ (*"number_of"*) _ _ = raise Match;
+ | numeral_tr' _ _ (*"number_of"*) _ _ = raise Match;
end;
@@ -86,6 +86,6 @@
val setup =
Sign.add_trfuns ([], [(@{syntax_const "_Numeral"}, numeral_tr)], [], []) #>
- Sign.add_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
+ Sign.add_advanced_trfunsT [(@{const_syntax Int.number_of}, numeral_tr')];
end;
--- a/src/HOL/Tools/record.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/Tools/record.ML Sun Sep 05 21:41:24 2010 +0200
@@ -699,9 +699,9 @@
val subst = Type.raw_matches (vartypes, argtypes) Vartab.empty
handle Type.TYPE_MATCH => err "type is no proper record (extension)";
+ val term_of_typ = Syntax.term_of_typ (Config.get ctxt show_sorts);
val alphas' =
- map (Syntax.term_of_typ (! Syntax.show_sorts) o Envir.norm_type subst o varifyT)
- (but_last alphas);
+ map (term_of_typ o Envir.norm_type subst o varifyT) (but_last alphas);
val more' = mk_ext rest;
in
@@ -810,7 +810,7 @@
val T = decode_type thy t;
val varifyT = varifyT (Term.maxidx_of_typ T);
- val term_of_type = Syntax.term_of_typ (! Syntax.show_sorts);
+ val term_of_type = Syntax.term_of_typ (Config.get ctxt show_sorts);
fun strip_fields T =
(case T of
@@ -856,7 +856,7 @@
fun mk_type_abbr subst name args =
let val abbrT = Type (name, map (varifyT o TFree) args)
- in Syntax.term_of_typ (! Syntax.show_sorts) (Envir.norm_type subst abbrT) end;
+ in Syntax.term_of_typ (Config.get ctxt show_sorts) (Envir.norm_type subst abbrT) end;
fun match rT T = Type.raw_match (varifyT rT, T) Vartab.empty;
in
--- a/src/HOL/ex/Numeral.thy Sun Sep 05 19:47:40 2010 +0200
+++ b/src/HOL/ex/Numeral.thy Sun Sep 05 21:41:24 2010 +0200
@@ -293,7 +293,7 @@
in [(@{syntax_const "_Numerals"}, numeral_tr)] end
*}
-typed_print_translation {*
+typed_print_translation (advanced) {*
let
fun dig b n = b + 2 * n;
fun int_of_num' (Const (@{const_syntax Dig0}, _) $ n) =
@@ -301,14 +301,15 @@
| int_of_num' (Const (@{const_syntax Dig1}, _) $ n) =
dig 1 (int_of_num' n)
| int_of_num' (Const (@{const_syntax One}, _)) = 1;
- fun num_tr' show_sorts T [n] =
+ fun num_tr' ctxt show_sorts T [n] =
let
val k = int_of_num' n;
val t' = Syntax.const @{syntax_const "_Numerals"} $ Syntax.free ("#" ^ string_of_int k);
- in case T
- of Type (@{type_name fun}, [_, T']) =>
- if not (! show_types) andalso can Term.dest_Type T' then t'
- else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
+ in
+ case T of
+ Type (@{type_name fun}, [_, T']) =>
+ if not (Config.get ctxt show_types) andalso can Term.dest_Type T' then t'
+ else Syntax.const Syntax.constrainC $ t' $ Syntax.term_of_typ show_sorts T'
| T' => if T' = dummyT then t' else raise Match
end;
in [(@{const_syntax of_num}, num_tr')] end
--- a/src/Pure/Isar/attrib.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Sun Sep 05 21:41:24 2010 +0200
@@ -392,7 +392,9 @@
(* theory setup *)
val _ = Context.>> (Context.map_theory
- (register_config Syntax.show_structs_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 #>
register_config Syntax.ambiguity_level_value #>
register_config Syntax.eta_contract_value #>
--- a/src/Pure/Isar/class.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/class.ML Sun Sep 05 21:41:24 2010 +0200
@@ -164,7 +164,7 @@
val Ss = Sorts.mg_domain algebra tyco [class];
in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
- ^ setmp_CRITICAL show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
+ ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
(SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
--- a/src/Pure/Isar/code.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/code.ML Sun Sep 05 21:41:24 2010 +0200
@@ -110,7 +110,8 @@
(* printing *)
-fun string_of_typ thy = setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy);
+fun string_of_typ thy =
+ Syntax.string_of_typ (Config.put show_sorts true (Syntax.init_pretty_global thy));
fun string_of_const thy c = case AxClass.inst_of_param thy c
of SOME (c, tyco) => Sign.extern_const thy c ^ " " ^ enclose "[" "]" (Sign.extern_type thy tyco)
--- a/src/Pure/Isar/locale.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/locale.ML Sun Sep 05 21:41:24 2010 +0200
@@ -180,7 +180,8 @@
fun prt_qual (qual, mand) = Pretty.str (qual ^ (if mand then "!" else "?"));
fun prt_quals qs = Pretty.separate "." (map prt_qual qs) |> Pretty.block;
val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
- fun prt_term' t = if !show_types
+ fun prt_term' t =
+ if Config.get ctxt show_types
then Pretty.block [prt_term t, Pretty.brk 1, Pretty.str "::",
Pretty.brk 1, (Pretty.quote o Syntax.pretty_typ ctxt) (type_of t)]
else prt_term t;
--- a/src/Pure/Isar/obtain.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Isar/obtain.ML Sun Sep 05 21:41:24 2010 +0200
@@ -215,7 +215,7 @@
val thy = ProofContext.theory_of ctxt;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
- val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term ctxt);
+ val string_of_term = Syntax.string_of_term (Config.put show_types true ctxt);
fun err msg th = error (msg ^ ":\n" ^ Display.string_of_thm ctxt th);
--- a/src/Pure/ProofGeneral/preferences.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/ProofGeneral/preferences.ML Sun Sep 05 21:41:24 2010 +0200
@@ -111,10 +111,10 @@
val display_preferences =
- [bool_pref show_types
+ [bool_pref show_types_default
"show-types"
"Include types in display of Isabelle terms",
- bool_pref show_sorts
+ bool_pref show_sorts_default
"show-sorts"
"Include sorts in display of Isabelle terms",
bool_pref show_consts_default
--- a/src/Pure/Syntax/printer.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Syntax/printer.ML Sun Sep 05 21:41:24 2010 +0200
@@ -7,8 +7,12 @@
signature PRINTER0 =
sig
val show_brackets: bool Unsynchronized.ref
- val show_sorts: bool Unsynchronized.ref
- val show_types: bool Unsynchronized.ref
+ 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
@@ -49,8 +53,14 @@
(** options for printing **)
-val show_types = Unsynchronized.ref false;
-val show_sorts = Unsynchronized.ref false;
+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;
+
+val show_sorts_default = Unsynchronized.ref false;
+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));
@@ -78,7 +88,7 @@
| app_first (f :: fs) = f ctxt args handle Match => app_first fs;
in app_first fns end;
-fun apply_typed x y fs = map (fn f => fn ctxt => f ctxt x y) fs;
+fun apply_typed x fs = map (fn f => fn ctxt => f ctxt (Config.get ctxt show_sorts) x) fs;
(* simple_ast_of *)
@@ -102,6 +112,7 @@
fun ast_of_termT ctxt trf tm =
let
+ val ctxt' = Config.put show_sorts false ctxt;
fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
| ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
| ast_of (Const (a, _)) = trans a []
@@ -111,19 +122,24 @@
| (f, args) => Ast.Appl (map ast_of (f :: args)))
| ast_of t = simple_ast_of ctxt t
and trans a args =
- ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
+ ast_of (apply_trans ctxt' (apply_typed dummyT (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
in ast_of tm end;
fun sort_to_ast ctxt trf S = ast_of_termT ctxt trf (Type_Ext.term_of_sort S);
-fun typ_to_ast ctxt trf T = ast_of_termT ctxt trf (Type_Ext.term_of_typ (! show_sorts) T);
+fun typ_to_ast ctxt trf T =
+ ast_of_termT ctxt trf (Type_Ext.term_of_typ (Config.get ctxt show_sorts) T);
(** term_to_ast **)
-fun ast_of_term idents consts ctxt trf show_types show_sorts tm =
+fun term_to_ast idents consts ctxt trf tm =
let
+ val show_types =
+ Config.get ctxt show_types orelse Config.get ctxt show_sorts orelse
+ Config.get ctxt show_all_types;
+ val show_sorts = Config.get ctxt show_sorts;
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;
@@ -188,7 +204,7 @@
| (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
and trans a T args =
- ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
+ ast_of (apply_trans ctxt (apply_typed T (trf a)) args)
handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
and constrain t T =
@@ -204,10 +220,6 @@
|> ast_of
end;
-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) tm;
-
(** type prtabs **)
--- a/src/Pure/Thy/thy_output.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/Thy/thy_output.ML Sun Sep 05 21:41:24 2010 +0200
@@ -444,8 +444,8 @@
(* options *)
-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_types" (Config.put show_types o boolean);
+val _ = add_option "show_sorts" (Config.put show_sorts 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);
--- a/src/Pure/axclass.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/axclass.ML Sun Sep 05 21:41:24 2010 +0200
@@ -519,7 +519,7 @@
fun check_constraint (a, S) =
if Sign.subsort thy (super, S) then ()
else error ("Sort constraint of type variable " ^
- setmp_CRITICAL show_sorts true (Syntax.string_of_typ ctxt) (TFree (a, S)) ^
+ Syntax.string_of_typ (Config.put show_sorts true ctxt) (TFree (a, S)) ^
" needs to be weaker than " ^ Syntax.string_of_sort ctxt super);
--- a/src/Pure/goal_display.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/goal_display.ML Sun Sep 05 21:41:24 2010 +0200
@@ -77,12 +77,20 @@
fun pretty_goals ctxt0 state =
let
- val ctxt = Config.put show_free_types false ctxt0;
+ val ctxt = ctxt0
+ |> Config.put show_free_types false
+ |> Config.put show_types
+ (Config.get ctxt0 show_types orelse
+ Config.get ctxt0 show_sorts orelse
+ Config.get ctxt0 show_all_types)
+ |> Config.put show_sorts false;
- val show_all_types = Config.get ctxt show_all_types;
+ val show_sorts0 = Config.get ctxt0 show_sorts;
+ val show_types = Config.get ctxt show_types;
+ val show_consts = Config.get ctxt show_consts
+ val show_main_goal = Config.get ctxt show_main_goal;
val goals_limit = Config.get ctxt goals_limit;
val goals_total = Config.get ctxt goals_total;
- val show_main_goal = Config.get ctxt show_main_goal;
val prt_sort = Syntax.pretty_sort ctxt;
val prt_typ = Syntax.pretty_typ ctxt;
@@ -120,23 +128,18 @@
val {prop, tpairs, ...} = Thm.rep_thm state;
val (As, B) = Logic.strip_horn prop;
val ngoals = length As;
-
- fun pretty_gs (types, sorts) =
- (if show_main_goal then [prt_term B] else []) @
- (if ngoals = 0 then [Pretty.str "No subgoals!"]
- else if ngoals > goals_limit then
- pretty_subgoals (take goals_limit As) @
- (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
- else [])
- else pretty_subgoals As) @
- pretty_ffpairs tpairs @
- (if Config.get ctxt show_consts then pretty_consts prop else []) @
- (if types then pretty_vars prop else []) @
- (if sorts then pretty_varsT prop else []);
in
- setmp_CRITICAL show_types (! show_types orelse ! show_sorts orelse show_all_types)
- (setmp_CRITICAL show_sorts false pretty_gs)
- (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts)
+ (if show_main_goal then [prt_term B] else []) @
+ (if ngoals = 0 then [Pretty.str "No subgoals!"]
+ else if ngoals > goals_limit then
+ pretty_subgoals (take goals_limit As) @
+ (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
+ else [])
+ else pretty_subgoals As) @
+ pretty_ffpairs tpairs @
+ (if show_consts then pretty_consts prop else []) @
+ (if show_types then pretty_vars prop else []) @
+ (if show_sorts0 then pretty_varsT prop else [])
end;
fun pretty_goals_without_context th =
--- a/src/Pure/theory.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Pure/theory.ML Sun Sep 05 21:41:24 2010 +0200
@@ -161,11 +161,13 @@
| TERM (msg, _) => error msg;
val _ = Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
+ val ctxt = Syntax.init_pretty_global thy
+ |> Config.put show_sorts true;
val bad_sorts =
rev ((fold_types o fold_atyps_sorts) (fn (_, []) => I | (T, _) => insert (op =) T) t []);
val _ = null bad_sorts orelse
error ("Illegal sort constraints in primitive specification: " ^
- commas (map (setmp_CRITICAL show_sorts true (Syntax.string_of_typ_global thy)) bad_sorts));
+ commas (map (Syntax.string_of_typ ctxt) bad_sorts));
in
(b, Sign.no_vars (Syntax.init_pretty_global thy) t)
end handle ERROR msg =>
@@ -217,18 +219,18 @@
handle TYPE (msg, _, _) => error msg;
val T' = Logic.varifyT_global T;
- fun message txt =
+ val ctxt = Syntax.init_pretty_global thy;
+ fun message sorts txt =
[Pretty.block [Pretty.str "Specification of constant ",
- Pretty.str c, Pretty.str " ::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ_global thy T)],
+ Pretty.str c, Pretty.str " ::", Pretty.brk 1,
+ Pretty.quote (Syntax.pretty_typ (Config.put show_sorts sorts ctxt) T)],
Pretty.str txt] |> Pretty.chunks |> Pretty.string_of;
in
if Sign.typ_instance thy (declT, T') then ()
else if Type.raw_instance (declT, T') then
- error (setmp_CRITICAL show_sorts true
- message "imposes additional sort constraints on the constant declaration")
+ error (message true "imposes additional sort constraints on the constant declaration")
else if overloaded then ()
- else warning (message "is strictly less general than the declared type");
- (c, T)
+ else warning (message false "is strictly less general than the declared type")
end;
@@ -272,7 +274,7 @@
| const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
| const_of _ = error "Attempt to finalize non-constant term";
fun specify (c, T) = dependencies thy false NONE (c ^ " axiom") (c, T) [];
- val finalize = specify o check_overloading thy overloaded o const_of o
+ val finalize = specify o tap (check_overloading thy overloaded) o const_of o
Sign.cert_term thy o prep_term thy;
in thy |> map_defs (fold finalize args) end;
--- a/src/Tools/nbe.ML Sun Sep 05 19:47:40 2010 +0200
+++ b/src/Tools/nbe.ML Sun Sep 05 21:41:24 2010 +0200
@@ -552,10 +552,11 @@
singleton (Type_Infer.infer_types (Syntax.pp_global thy) (Sign.tsig_of thy) I
(try (Type.strip_sorts o Sign.the_const_type thy)) (K NONE) Name.context 0)
(Type_Infer.constrain ty' t);
- fun check_tvars t = if null (Term.add_tvars t []) then t else
- error ("Illegal schematic type variables in normalized term: "
- ^ setmp_CRITICAL show_types true (Syntax.string_of_term_global thy) t);
- val string_of_term = setmp_CRITICAL show_types true (Syntax.string_of_term_global thy);
+ val string_of_term =
+ Syntax.string_of_term (Config.put show_types true (Syntax.init_pretty_global thy));
+ fun check_tvars t =
+ if null (Term.add_tvars t []) then t
+ else error ("Illegal schematic type variables in normalized term: " ^ string_of_term t);
in
compile_eval thy program (vs, t) deps
|> traced (fn t => "Normalized:\n" ^ string_of_term t)