src/Pure/Thy/sessions.scala
changeset 66714 9fc4e144693c
parent 66712 4c98c929a12a
child 66715 6bced18e2b91
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:03:33 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 17:28:44 2017 +0200
     1.3 @@ -205,7 +205,7 @@
     1.4  
     1.5              val syntax = thy_deps.syntax
     1.6  
     1.7 -            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
     1.8 +            val theory_files = thy_deps.entries.map(entry => Path.explode(entry.name.node))
     1.9              val loaded_files =
    1.10                if (inlined_files) {
    1.11                  if (Sessions.is_pure(info.name)) {
    1.12 @@ -251,18 +251,18 @@
    1.13                        val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
    1.14                        ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.15  
    1.16 -              (graph0 /: thy_deps.deps)(
    1.17 -                { case (g, dep) =>
    1.18 -                    val a = node(dep.name)
    1.19 +              (graph0 /: thy_deps.entries)(
    1.20 +                { case (g, entry) =>
    1.21 +                    val a = node(entry.name)
    1.22                      val bs =
    1.23 -                      dep.header.imports.map({ case (name, _) => node(name) }).
    1.24 +                      entry.header.imports.map({ case (name, _) => node(name) }).
    1.25                          filterNot(_ == a)
    1.26                      ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
    1.27              }
    1.28  
    1.29              val known =
    1.30                Known.make(info.dir, List(imports_base),
    1.31 -                theories = thy_deps.deps.map(_.name),
    1.32 +                theories = thy_deps.entries.map(_.name),
    1.33                  loaded_files = loaded_files)
    1.34  
    1.35              val sources =