src/Pure/Thy/sessions.scala
changeset 66828 3c936ebebc23
parent 66823 f529719cc47d
child 66829 5baca4c94737
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Oct 09 22:08:05 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Tue Oct 10 11:20:02 2017 +0200
     1.3 @@ -267,8 +267,7 @@
     1.4                }
     1.5  
     1.6                val imports_subgraph =
     1.7 -                sessions.imports_graph.restrict(
     1.8 -                  sessions.imports_graph.all_preds(info.parent.toList ::: info.imports).toSet)
     1.9 +                sessions.imports_graph.restrict(sessions.imports_graph.all_preds(info.deps).toSet)
    1.10  
    1.11                val graph0 =
    1.12                  (Graph_Display.empty_graph /: imports_subgraph.topological_order)(
    1.13 @@ -369,6 +368,8 @@
    1.14      document_files: List[(Path, Path)],
    1.15      meta_digest: SHA1.Digest)
    1.16    {
    1.17 +    def deps: List[String] = parent.toList ::: imports
    1.18 +
    1.19      def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
    1.20    }
    1.21