# HG changeset patch
# User wenzelm
# Date 1279713344 -7200
# Node ID cd1d1bc7684cdde1ef9e6720eb0eeb0363d70c48
# Parent  3a6ec95a9f68764525653793a31b1013e01b97d0
thy_deps: more direct comparison of sessions, which is presumably what "unfold" is meant to indicate here -- also avoid referring to accidental theory loader state;

diff -r 3a6ec95a9f68 -r cd1d1bc7684c src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 13:25:14 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Wed Jul 21 13:55:44 2010 +0200
@@ -408,14 +408,16 @@
 val thy_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>
   let
     val thy = Toplevel.theory_of state;
+    val thy_session = Present.session_name thy;
+
     val all_thys = sort Thy_Info.thy_ord (thy :: Theory.ancestors_of thy);
     val gr = all_thys |> map (fn node =>
       let
         val name = Context.theory_name node;
         val parents = map Context.theory_name (Theory.parents_of node);
-        val dir = Present.session_name node;
-        val unfold = not (Thy_Info.known_thy name andalso Thy_Info.is_finished name);
-      in {name = name, ID = name, parents = parents, dir = dir, unfold = unfold, path = ""} end);
+        val session = Present.session_name node;
+        val unfold = (session = thy_session);
+      in {name = name, ID = name, parents = parents, dir = session, unfold = unfold, path = ""} end);
   in Present.display_graph gr end);
 
 val class_deps = Toplevel.unknown_theory o Toplevel.keep (fn state =>