# HG changeset patch
# User wenzelm
# Date 1507627202 -7200
# Node ID 3c936ebebc23c50526d400bbe7061484049393ae
# Parent  9f6ec65f7a6efd25dbd39024aecc91f84aaf0631
tuned signature;

diff -r 9f6ec65f7a6e -r 3c936ebebc23 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Oct 09 22:08:05 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 11:20:02 2017 +0200
@@ -267,8 +267,7 @@
               }
 
               val imports_subgraph =
-                sessions.imports_graph.restrict(
-                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
+                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
 
               val graph0 =
                 (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
@@ -369,6 +368,8 @@
     document_files: List[(Path, Path)],
     meta_digest: SHA1.Digest)
   {
+    def deps: List[String] = parent.toList ::: imports
+
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }