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;
authorwenzelm
Wed, 21 Jul 2010 13:55:44 +0200
changeset 37866 cd1d1bc7684c
parent 37865 3a6ec95a9f68
child 37867 b9783e9e96e1
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;
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 =>