new display of theory stamps

--- a/src/Pure/Isar/toplevel.ML	Sat Mar 26 16:14:17 2005 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Mar 26 18:20:29 2005 +0100
@@ -98,7 +98,7 @@
 
 fun pretty_context thy = [Pretty.block
   [Pretty.str "theory", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
-    Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]];
+    Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]];
 
 fun pretty_prf prf = Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf);
 

--- a/src/Pure/Thy/thy_info.ML	Sat Mar 26 16:14:17 2005 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Mar 26 18:20:29 2005 +0100
@@ -47,6 +47,8 @@
   val end_theory: theory -> theory
   val finish: unit -> unit
   val register_theory: theory -> unit
+  val pretty_theory: theory -> Pretty.T
+  val pprint_theory: theory -> pprint_args -> unit
 end;
 
 structure ThyInfo: THY_INFO =
@@ -165,6 +167,19 @@
     error (loader_msg "nothing known about theory" [name]);
 
 
+(* pretty printing a theory: omit finished theories *)
+
+fun unfinished_names stamps =
+    List.last (List.filter is_finished stamps) :: List.filter (not o is_finished) stamps;
+
+fun pretty_sg sg = 
+      Pretty.str_list "{" "}" 
+        (unfinished_names (List.filter known_thy (Sign.stamp_names_of sg)));
+
+val pretty_theory = pretty_sg o Theory.sign_of;
+val pprint_theory = Pretty.pprint o pretty_theory;
+
+
 (* access theory *)
 
 fun lookup_theory name =

--- a/src/Pure/install_pp.ML	Sat Mar 26 16:14:17 2005 +0100
+++ b/src/Pure/install_pp.ML	Sat Mar 26 18:20:29 2005 +0100
@@ -4,7 +4,7 @@
 Set up automatic toplevel pretty printing.
 *)
 
-install_pp (make_pp ["Theory", "theory"] Display.pprint_theory);
+install_pp (make_pp ["Theory", "theory"] ThyInfo.pprint_theory);
 install_pp (make_pp ["Thm", "thm"] Display.pprint_thm);
 install_pp (make_pp ["Thm", "cterm"] Display.pprint_cterm);
 install_pp (make_pp ["Thm", "ctyp"] Display.pprint_ctyp);