1.1 --- a/src/Pure/Isar/proof_context.ML Thu Mar 26 14:14:02 2009 +0100
1.2 +++ b/src/Pure/Isar/proof_context.ML Thu Mar 26 15:18:50 2009 +0100
1.3 @@ -36,6 +36,9 @@
1.4 val theory_result: (theory -> 'a * theory) -> Proof.context -> 'a * Proof.context
1.5 val extern_fact: Proof.context -> string -> xstring
1.6 val pretty_term_abbrev: Proof.context -> term -> Pretty.T
1.7 + val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T
1.8 + val pretty_thms_aux: Proof.context -> bool -> thm list -> Pretty.T
1.9 + val pretty_fact_aux: Proof.context -> bool -> string * thm list -> Pretty.T
1.10 val pretty_thm: Proof.context -> thm -> Pretty.T
1.11 val pretty_thms: Proof.context -> thm list -> Pretty.T
1.12 val pretty_fact: Proof.context -> string * thm list -> Pretty.T
1.13 @@ -295,21 +298,28 @@
1.14
1.15 fun pretty_term_abbrev ctxt = Syntax.pretty_term (set_mode mode_abbrev ctxt);
1.16
1.17 -fun pretty_thm ctxt th =
1.18 - let val asms = map Thm.term_of (Assumption.all_assms_of ctxt)
1.19 - in Display.pretty_thm_aux (Syntax.pp ctxt) false true asms th end;
1.20 +fun pretty_thm_aux ctxt show_status th =
1.21 + let
1.22 + val flags = {quote = false, show_hyps = true, show_status = show_status};
1.23 + val asms = map Thm.term_of (Assumption.all_assms_of ctxt);
1.24 + in Display.pretty_thm_aux (Syntax.pp ctxt) flags asms th end;
1.25
1.26 -fun pretty_thms ctxt [th] = pretty_thm ctxt th
1.27 - | pretty_thms ctxt ths = Pretty.blk (0, Pretty.fbreaks (map (pretty_thm ctxt) ths));
1.28 +fun pretty_thms_aux ctxt flag [th] = pretty_thm_aux ctxt flag th
1.29 + | pretty_thms_aux ctxt flag ths =
1.30 + Pretty.blk (0, Pretty.fbreaks (map (pretty_thm_aux ctxt flag) ths));
1.31
1.32 fun pretty_fact_name ctxt a = Pretty.block
1.33 [Pretty.markup (Markup.fact a) [Pretty.str (extern_fact ctxt a)], Pretty.str ":"];
1.34
1.35 -fun pretty_fact ctxt ("", ths) = pretty_thms ctxt ths
1.36 - | pretty_fact ctxt (a, [th]) = Pretty.block
1.37 - [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm ctxt th]
1.38 - | pretty_fact ctxt (a, ths) = Pretty.block
1.39 - (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm ctxt) ths));
1.40 +fun pretty_fact_aux ctxt flag ("", ths) = pretty_thms_aux ctxt flag ths
1.41 + | pretty_fact_aux ctxt flag (a, [th]) = Pretty.block
1.42 + [pretty_fact_name ctxt a, Pretty.brk 1, pretty_thm_aux ctxt flag th]
1.43 + | pretty_fact_aux ctxt flag (a, ths) = Pretty.block
1.44 + (Pretty.fbreaks (pretty_fact_name ctxt a :: map (pretty_thm_aux ctxt flag) ths));
1.45 +
1.46 +fun pretty_thm ctxt = pretty_thm_aux ctxt true;
1.47 +fun pretty_thms ctxt = pretty_thms_aux ctxt true;
1.48 +fun pretty_fact ctxt = pretty_fact_aux ctxt true;
1.49
1.50 val string_of_thm = Pretty.string_of oo pretty_thm;
1.51
2.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 14:14:02 2009 +0100
2.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Mar 26 15:18:50 2009 +0100
2.3 @@ -655,13 +655,9 @@
2.4 text=[XML.Elem("pgml",[],
2.5 maps YXML.parse_body strings)] })
2.6
2.7 - fun string_of_thm th = Pretty.string_of
2.8 - (Display.pretty_thm_aux
2.9 - (Syntax.pp_global (Thm.theory_of_thm th))
2.10 - false (* quote *)
2.11 - false (* show hyps *)
2.12 - [] (* asms *)
2.13 - th)
2.14 + fun string_of_thm th = Pretty.string_of (Display.pretty_thm_aux
2.15 + (Syntax.pp_global (Thm.theory_of_thm th))
2.16 + {quote = false, show_hyps = false, show_status = true} [] th)
2.17
2.18 fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name)
2.19
3.1 --- a/src/Pure/display.ML Thu Mar 26 14:14:02 2009 +0100
3.2 +++ b/src/Pure/display.ML Thu Mar 26 15:18:50 2009 +0100
3.3 @@ -17,7 +17,8 @@
3.4 sig
3.5 include BASIC_DISPLAY
3.6 val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T
3.7 - val pretty_thm_aux: Pretty.pp -> bool -> bool -> term list -> thm -> Pretty.T
3.8 + val pretty_thm_aux: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} ->
3.9 + term list -> thm -> Pretty.T
3.10 val pretty_thm: thm -> Pretty.T
3.11 val string_of_thm: thm -> string
3.12 val pretty_thms: thm list -> Pretty.T
3.13 @@ -57,19 +58,20 @@
3.14 fun pretty_flexpair pp (t, u) = Pretty.block
3.15 [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u];
3.16
3.17 -fun display_status th =
3.18 - let
3.19 - val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
3.20 - val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
3.21 - in
3.22 - if failed then "!!"
3.23 - else if oracle andalso unfinished then "!?"
3.24 - else if oracle then "!"
3.25 - else if unfinished then "?"
3.26 - else ""
3.27 - end;
3.28 +fun display_status false _ = ""
3.29 + | display_status true th =
3.30 + let
3.31 + val {oracle = oracle0, unfinished, failed} = Thm.status_of th;
3.32 + val oracle = oracle0 andalso (not (! quick_and_dirty) orelse ! show_hyps);
3.33 + in
3.34 + if failed then "!!"
3.35 + else if oracle andalso unfinished then "!?"
3.36 + else if oracle then "!"
3.37 + else if unfinished then "?"
3.38 + else ""
3.39 + end;
3.40
3.41 -fun pretty_thm_aux pp quote show_hyps' asms raw_th =
3.42 +fun pretty_thm_aux pp {quote, show_hyps = show_hyps', show_status} asms raw_th =
3.43 let
3.44 val th = Thm.strip_shyps raw_th;
3.45 val {hyps, tpairs, prop, ...} = Thm.rep_thm th;
3.46 @@ -80,7 +82,7 @@
3.47 val prt_term = q o Pretty.term pp;
3.48
3.49 val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps;
3.50 - val status = display_status th;
3.51 + val status = display_status show_status th;
3.52
3.53 val hlen = length xshyps + length hyps' + length tpairs;
3.54 val hsymbs =
3.55 @@ -97,7 +99,8 @@
3.56 in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end;
3.57
3.58 fun pretty_thm th =
3.59 - pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th)) true false [] th;
3.60 + pretty_thm_aux (Syntax.pp_global (Thm.theory_of_thm th))
3.61 + {quote = true, show_hyps = false, show_status = true} [] th;
3.62
3.63 val string_of_thm = Pretty.string_of o pretty_thm;
3.64