# HG changeset patch
# User wenzelm
# Date 1116852997 -7200
# Node ID b2bf9a5cde37b063e002a5bc9359334a70cfaa32
# Parent  7d68cd1b1b8b7710012a3d71f231d2b24dcf12e0
tuned pretty_sg;
tuned;

diff -r 7d68cd1b1b8b -r b2bf9a5cde37 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Mon May 23 14:56:36 2005 +0200
+++ b/src/Pure/Thy/thy_info.ML	Mon May 23 14:56:37 2005 +0200
@@ -95,7 +95,6 @@
 fun update_node name parents entry G =
   (if can (Graph.get_node G) name then upd_deps name entry G else Graph.new_node (name, entry) G)
   |> add_deps name parents;
-   
 
 
 (* thy database *)
@@ -135,7 +134,7 @@
 fun lookup_thy name =
   SOME (thy_graph Graph.get_node name) handle Graph.UNDEF _ => NONE;
 
-val known_thy = isSome o lookup_thy;
+val known_thy = is_some o lookup_thy;
 fun check_known_thy name = known_thy name orelse (warning ("Unknown theory " ^ quote name); false);
 fun if_known_thy f name = if check_known_thy name then f name else ();
 
@@ -168,18 +167,27 @@
     error (loader_msg "nothing known about theory" [name]);
 
 
-(* pretty printing a theory: omit finished theories *)
+(* pretty printing a theory *)
+
+local
 
-fun unfinished_names stamps =
-    List.last (List.filter is_finished stamps) :: List.filter (not o is_finished) stamps;
+fun relevant_names names =
+  let
+    val (finished, unfinished) =
+      List.filter (equal "#" orf known_thy) names
+      |> List.partition (not_equal "#" andf is_finished);
+  in (if not (null finished) then [List.last finished] else []) @ unfinished end;
 
-fun pretty_sg sg = 
-      Pretty.str_list "{" "}" 
-        (unfinished_names (List.filter known_thy (Sign.stamp_names_of sg)));
+fun pretty_sg sg =
+  Pretty.str_list "{" "}" (relevant_names (Sign.stamp_names_of sg));
+
+in
 
 val pretty_theory = pretty_sg o Theory.sign_of;
 val pprint_theory = Pretty.pprint o pretty_theory;
 
+end;
+
 
 (* access theory *)
 
@@ -244,8 +252,8 @@
 (* load_file *)
 
 val opt_path = Option.map (Path.dir o fst o ThyLoad.get_thy);
-fun opt_path' (d : deps option) = getOpt (Option.map (opt_path o #master) d, NONE);
-fun opt_path'' d = getOpt (Option.map opt_path' d, NONE);
+fun opt_path' (d: deps option) = if_none (Option.map (opt_path o #master) d) NONE;
+fun opt_path'' d = if_none (Option.map opt_path' d) NONE;
 
 local
 
@@ -360,7 +368,7 @@
         val (current, (new_deps, parents)) = current_deps ml strict dir name handle ERROR =>
           error (loader_msg "the error(s) above occurred while examining theory" [name] ^
             (if null initiators then "" else required_by "\n" initiators));
-        val dir' = getOpt (opt_path'' new_deps, dir);
+        val dir' = if_none (opt_path'' new_deps) dir;
         val (visited', parent_results) = foldl_map (req_parent dir') (name :: visited, parents);
 
         val thy = if not really then SOME (get_theory name) else NONE;
@@ -417,7 +425,7 @@
   let
     val bparents = map base_of_path parents;
     val dir' = opt_path'' (lookup_deps name);
-    val dir = getOpt (dir',Path.current);
+    val dir = if_none dir' Path.current;
     val assert_thy = if upd then quiet_update_thy' true dir else weak_use_thy dir;
     val _ = check_unfinished error name;
     val _ = List.app assert_thy parents;