# HG changeset patch
# User wenzelm
# Date 1144922470 -7200
# Node ID cae7cc0729946f9ad5a66f9ad53b0ef3448284b4
# Parent  20e86336a53f3cae1aad5b81a1a5fa466c45c4b0
added print_theorems/theory, print_theorems_diff (from pure_thy.ML);

diff -r 20e86336a53f -r cae7cc072994 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Thu Apr 13 12:01:09 2006 +0200
+++ b/src/Pure/Isar/proof_display.ML	Thu Apr 13 12:01:10 2006 +0200
@@ -2,11 +2,19 @@
     ID:         $Id$
     Author:     Makarius
 
-Printing of Isar proof configurations etc.
+Printing of theorems, goals, results etc.
 *)
 
+signature BASIC_PROOF_DISPLAY =
+sig
+  val print_theorems: theory -> unit
+  val print_theory: theory -> unit
+end
+
 signature PROOF_DISPLAY =
 sig
+  include BASIC_PROOF_DISPLAY
+  val print_theorems_diff: theory -> theory -> unit
   val string_of_rule: ProofContext.context -> string -> thm -> string
   val print_results: bool -> ProofContext.context ->
     ((string * string) * (string * thm list) list) -> unit
@@ -17,6 +25,29 @@
 structure ProofDisplay: PROOF_DISPLAY =
 struct
 
+
+(* theorems and theory *)
+
+fun pretty_theorems_diff prev_thms thy =
+  let
+    val ctxt = ProofContext.init thy;
+    val (space, thms) = PureThy.theorems_of thy;
+    val diff_thmss = Symtab.fold (fn fact =>
+      if not (Symtab.member Thm.eq_thms prev_thms fact) then cons fact else I) thms [];
+    val thmss = diff_thmss |> map (apfst (NameSpace.extern space)) |> Library.sort_wrt #1;
+  in Pretty.big_list "theorems:" (map (ProofContext.pretty_fact ctxt) thmss) end;
+
+fun print_theorems_diff prev_thy thy =
+  Pretty.writeln (pretty_theorems_diff (#2 (PureThy.theorems_of prev_thy)) thy);
+
+fun pretty_theorems thy = pretty_theorems_diff Symtab.empty thy;
+
+val print_theorems = Pretty.writeln o pretty_theorems;
+
+fun print_theory thy =
+  Pretty.writeln (Pretty.chunks (Display.pretty_full_theory thy @ [pretty_theorems thy]));
+
+
 (* refinement rule *)
 
 fun pretty_rule ctxt s thm =
@@ -73,3 +104,7 @@
 end;
 
 end;
+
+structure BasicProofDisplay: BASIC_PROOF_DISPLAY = ProofDisplay;
+open BasicProofDisplay;
+