--- a/src/HOL/Tools/inductive.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/HOL/Tools/inductive.ML Sat Mar 30 13:40:19 2013 +0100
@@ -224,8 +224,7 @@
(Pretty.breaks
(Pretty.str "(co)inductives:" ::
map (Pretty.mark_str o #1) (Name_Space.extern_table ctxt (space, infos)))),
- Pretty.big_list "monotonicity rules:"
- (map (Pretty.item o single o Display.pretty_thm ctxt) monos)]
+ Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_item ctxt) monos)]
end |> Pretty.chunks |> Pretty.writeln;
--- a/src/Provers/classical.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Provers/classical.ML Sat Mar 30 13:40:19 2013 +0100
@@ -609,7 +609,7 @@
fun print_claset ctxt =
let
val {safeIs, safeEs, hazIs, hazEs, swrappers, uwrappers, ...} = rep_claset_of ctxt;
- val pretty_thms = map (Pretty.item o single o Display.pretty_thm ctxt) o Item_Net.content;
+ val pretty_thms = map (Display.pretty_thm_item ctxt) o Item_Net.content;
in
[Pretty.big_list "safe introduction rules (intro!):" (pretty_thms safeIs),
Pretty.big_list "introduction rules (intro):" (pretty_thms hazIs),
--- a/src/Pure/Isar/calculation.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/calculation.ML Sat Mar 30 13:40:19 2013 +0100
@@ -40,11 +40,12 @@
val get_rules = #1 o Data.get o Context.Proof;
fun print_rules ctxt =
- let val (trans, sym) = get_rules ctxt in
- [Pretty.big_list "transitivity rules:"
- (map (Pretty.item o single o Display.pretty_thm ctxt) (Item_Net.content trans)),
- Pretty.big_list "symmetry rules:"
- (map (Pretty.item o single o Display.pretty_thm ctxt) sym)]
+ let
+ val pretty_thm = Display.pretty_thm_item ctxt;
+ val (trans, sym) = get_rules ctxt;
+ in
+ [Pretty.big_list "transitivity rules:" (map pretty_thm (Item_Net.content trans)),
+ Pretty.big_list "symmetry rules:" (map pretty_thm sym)]
end |> Pretty.chunks |> Pretty.writeln;
@@ -130,6 +131,7 @@
let
val ctxt = Proof.context_of state;
val pretty_thm = Display.pretty_thm ctxt;
+ val pretty_thm_item = Display.pretty_thm_item ctxt;
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
@@ -142,7 +144,7 @@
[Pretty.block [Pretty.str "Vacuous calculation result:", Pretty.brk 1, pretty_thm th],
(Pretty.block o Pretty.fbreaks)
(Pretty.str ("derived as projection (" ^ string_of_int (i + 1) ^ ") from:") ::
- map pretty_thm ths)]));
+ map pretty_thm_item ths)]));
val opt_rules = Option.map (prep_rules ctxt) raw_rules;
fun combine ths =
@@ -158,7 +160,7 @@
(Seq.single (Seq.Error (fn () =>
(Pretty.string_of o Pretty.block o Pretty.fbreaks)
(Pretty.str "No matching trans rules for calculation:" ::
- map pretty_thm ths))));
+ map pretty_thm_item ths))));
val facts = Proof.the_facts (assert_sane final state);
val (initial, calculations) =
--- a/src/Pure/Isar/code.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/code.ML Sat Mar 30 13:40:19 2013 +0100
@@ -954,10 +954,8 @@
val ctxt = Proof_Context.init_global thy;
val exec = the_exec thy;
fun pretty_equations const thms =
- (Pretty.block o Pretty.fbreaks) (
- Pretty.str (string_of_const thy const) ::
- map (Pretty.item o single o Display.pretty_thm ctxt) thms
- );
+ (Pretty.block o Pretty.fbreaks)
+ (Pretty.str (string_of_const thy const) :: map (Display.pretty_thm_item ctxt) thms);
fun pretty_function (const, Default (_, eqns_lazy)) =
pretty_equations const (map fst (Lazy.force eqns_lazy))
| pretty_function (const, Eqns eqns) = pretty_equations const (map fst eqns)
--- a/src/Pure/Isar/context_rules.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/context_rules.ML Sat Mar 30 13:40:19 2013 +0100
@@ -117,7 +117,7 @@
fun prt_kind (i, b) =
Pretty.big_list ((the o AList.lookup (op =) kind_names) (i, b) ^ ":")
(map_filter (fn (_, (k, th)) =>
- if k = (i, b) then SOME (Pretty.item [Display.pretty_thm ctxt th]) else NONE)
+ if k = (i, b) then SOME (Display.pretty_thm_item ctxt th) else NONE)
(sort (int_ord o pairself fst) rules));
in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
--- a/src/Pure/Isar/local_defs.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/local_defs.ML Sat Mar 30 13:40:19 2013 +0100
@@ -181,7 +181,7 @@
fun print_rules ctxt =
Pretty.writeln (Pretty.big_list "definitional transformations:"
- (map (Display.pretty_thm ctxt) (Rules.get (Context.Proof ctxt))));
+ (map (Display.pretty_thm_item ctxt) (Rules.get (Context.Proof ctxt))));
val defn_add = Thm.declaration_attribute (Rules.map o Thm.add_thm);
val defn_del = Thm.declaration_attribute (Rules.map o Thm.del_thm);
--- a/src/Pure/Isar/method.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/method.ML Sat Mar 30 13:40:19 2013 +0100
@@ -202,7 +202,7 @@
fun trace ctxt rules =
if Config.get ctxt rule_trace andalso not (null rules) then
- Pretty.big_list "rules:" (map (Display.pretty_thm ctxt) rules)
+ Pretty.big_list "rules:" (map (Display.pretty_thm_item ctxt) rules)
|> Pretty.string_of |> tracing
else ();
--- a/src/Pure/Isar/proof.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/proof.ML Sat Mar 30 13:40:19 2013 +0100
@@ -337,12 +337,7 @@
(** pretty_state **)
fun pretty_facts _ _ NONE = []
- | pretty_facts s ctxt (SOME ths) =
- [(Pretty.block o Pretty.fbreaks)
- ((if s = "" then Pretty.str "this:"
- else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
- map (Display.pretty_thm ctxt) ths),
- Pretty.str ""];
+ | pretty_facts ctxt s (SOME ths) = [Proof_Display.pretty_goal_facts ctxt s ths, Pretty.str ""];
fun pretty_state nr state =
let
@@ -351,7 +346,7 @@
fun prt_goal (SOME (_, (_,
{statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
- pretty_facts "using" ctxt
+ pretty_facts ctxt "using"
(if mode <> Backward orelse null using then NONE else SOME using) @
[Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
(map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
@@ -367,8 +362,8 @@
Pretty.str ""] @
(if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @
(if verbose orelse mode = Forward then
- pretty_facts "" ctxt facts @ prt_goal (try find_goal state)
- else if mode = Chain then pretty_facts "picking" ctxt facts
+ pretty_facts ctxt "" facts @ prt_goal (try find_goal state)
+ else if mode = Chain then pretty_facts ctxt "picking" facts
else prt_goal (try find_goal state))
end;
--- a/src/Pure/Isar/proof_context.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/proof_context.ML Sat Mar 30 13:40:19 2013 +0100
@@ -345,7 +345,7 @@
fun pretty_fact ctxt =
let
val pretty_thm = Display.pretty_thm ctxt;
- val pretty_thms = map (Pretty.item o single o pretty_thm);
+ val pretty_thms = map (Display.pretty_thm_item ctxt);
in
fn ("", [th]) => pretty_thm th
| ("", ths) => Pretty.blk (0, Pretty.fbreaks (pretty_thms ths))
@@ -1314,10 +1314,10 @@
Pretty.commas (map prt_fix fixes))];
(*prems*)
- val prems = Assumption.all_prems_of ctxt;
val prt_prems =
- if null prems then []
- else [Pretty.big_list "prems:" (map (Display.pretty_thm ctxt) prems)];
+ (case Assumption.all_prems_of ctxt of
+ [] => []
+ | prems => [Pretty.big_list "prems:" (map (Display.pretty_thm_item ctxt) prems)]);
in prt_structs @ prt_fixes @ prt_prems end;
--- a/src/Pure/Isar/proof_display.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/Isar/proof_display.ML Sat Mar 30 13:40:19 2013 +0100
@@ -19,6 +19,7 @@
val string_of_rule: Proof.context -> string -> thm -> string
val pretty_goal_header: thm -> Pretty.T
val string_of_goal: Proof.context -> thm -> string
+ val pretty_goal_facts: Proof.context -> string -> thm list -> Pretty.T
val method_error: string -> Position.T ->
{context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
val print_results: Markup.T -> bool -> Proof.context ->
@@ -108,6 +109,15 @@
[pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
+(* goal facts *)
+
+fun pretty_goal_facts ctxt s ths =
+ (Pretty.block o Pretty.fbreaks)
+ ((if s = "" then Pretty.str "this:"
+ else Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"]) ::
+ map (Display.pretty_thm_item ctxt) ths);
+
+
(* method_error *)
fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
@@ -117,10 +127,7 @@
"proof method" ^ Position.here pos ^ ":\n";
val pr_facts =
if null facts then ""
- else
- (Pretty.string_of o Pretty.block o Pretty.fbreaks)
- (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
- map (Display.pretty_thm ctxt) facts) ^ "\n";
+ else Pretty.string_of (pretty_goal_facts ctxt "using" facts) ^ "\n";
val pr_goal = string_of_goal ctxt goal;
in pr_header ^ pr_facts ^ pr_goal end);
--- a/src/Pure/display.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/display.ML Sat Mar 30 13:40:19 2013 +0100
@@ -20,6 +20,7 @@
include BASIC_DISPLAY
val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool} -> thm -> Pretty.T
val pretty_thm: Proof.context -> thm -> Pretty.T
+ val pretty_thm_item: Proof.context -> thm -> Pretty.T
val pretty_thm_global: theory -> thm -> Pretty.T
val pretty_thm_without_context: thm -> Pretty.T
val string_of_thm: Proof.context -> thm -> string
@@ -79,6 +80,7 @@
in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
fun pretty_thm ctxt = pretty_thm_raw ctxt {quote = false, show_hyps = true};
+fun pretty_thm_item ctxt th = Pretty.item [pretty_thm ctxt th];
fun pretty_thm_global thy =
pretty_thm_raw (Syntax.init_pretty_global thy) {quote = false, show_hyps = false};
--- a/src/Pure/simplifier.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Pure/simplifier.ML Sat Mar 30 13:40:19 2013 +0100
@@ -121,6 +121,8 @@
let
val pretty_cterm = Syntax.pretty_term ctxt o Thm.term_of;
val pretty_thm = Display.pretty_thm ctxt;
+ val pretty_thm_item = Display.pretty_thm_item ctxt;
+
fun pretty_proc (name, lhss) =
Pretty.big_list (name ^ ":") (map (Pretty.item o single o pretty_cterm) lhss);
fun pretty_cong (name, thm) =
@@ -128,7 +130,7 @@
val {simps, procs, congs, loopers, unsafe_solvers, safe_solvers, ...} = dest_ss ss;
in
- [Pretty.big_list "simplification rules:" (map (Pretty.item o single o pretty_thm o #2) simps),
+ [Pretty.big_list "simplification rules:" (map (pretty_thm_item o #2) simps),
Pretty.big_list "simplification procedures:" (map pretty_proc (sort_wrt #1 procs)),
Pretty.big_list "congruences:" (map pretty_cong congs),
Pretty.strs ("loopers:" :: map quote loopers),
--- a/src/Tools/induct.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/Tools/induct.ML Sat Mar 30 13:40:19 2013 +0100
@@ -213,7 +213,7 @@
fun pretty_rules ctxt kind rs =
let val thms = map snd (Item_Net.content rs)
- in Pretty.big_list kind (map (Pretty.item o single o Display.pretty_thm ctxt) thms) end;
+ in Pretty.big_list kind (map (Display.pretty_thm_item ctxt) thms) end;
(* context data *)
--- a/src/ZF/Tools/typechk.ML Sat Mar 30 12:13:39 2013 +0100
+++ b/src/ZF/Tools/typechk.ML Sat Mar 30 13:40:19 2013 +0100
@@ -62,7 +62,7 @@
fun print_tcset ctxt =
let val TC {rules, ...} = tcset_of ctxt in
Pretty.writeln (Pretty.big_list "type-checking rules:"
- (map (Display.pretty_thm ctxt) rules))
+ (map (Display.pretty_thm_item ctxt) rules))
end;