--- 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 =