proper imports_base, notably for thy_deps;
authorwenzelm
Mon Apr 17 20:12:20 2017 +0200 (2017-04-17)
changeset 65496ca8dcb2a500c
parent 65495 60d4fbed2b1f
child 65497 7966bd7c6461
proper imports_base, notably for thy_deps;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Mon Apr 17 19:44:13 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Mon Apr 17 20:12:20 2017 +0200
     1.3 @@ -143,12 +143,16 @@
     1.4            if (progress.stopped) throw Exn.Interrupt()
     1.5  
     1.6            try {
     1.7 -            val parent_base =
     1.8 +            val parent_base: Sessions.Base =
     1.9                info.parent match {
    1.10                  case None => Base.bootstrap(global_theories)
    1.11                  case Some(parent) => session_bases(parent)
    1.12                }
    1.13 -            val resources = new Resources(parent_base,
    1.14 +            val imports_base: Sessions.Base =
    1.15 +              parent_base.copy(known =
    1.16 +                Known.make(info.dir, parent_base :: info.imports.map(session_bases(_)), Nil))
    1.17 +
    1.18 +            val resources = new Resources(imports_base,
    1.19                default_qualifier = info.theory_qualifier(session_name))
    1.20  
    1.21              if (verbose || list_files) {
    1.22 @@ -173,11 +177,6 @@
    1.23                }
    1.24              }
    1.25  
    1.26 -            val known =
    1.27 -              Known.make(info.dir,
    1.28 -                parent_base :: info.imports.map(session_bases(_)),
    1.29 -                thy_deps.deps.map(_.name))
    1.30 -
    1.31              val syntax = thy_deps.syntax
    1.32  
    1.33              val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
    1.34 @@ -210,11 +209,11 @@
    1.35              val base =
    1.36                Base(global_theories = global_theories,
    1.37                  loaded_theories = thy_deps.loaded_theories,
    1.38 -                known = known,
    1.39 +                known = Known.make(info.dir, List(imports_base), thy_deps.deps.map(_.name)),
    1.40                  keywords = thy_deps.keywords,
    1.41                  syntax = syntax,
    1.42                  sources = all_files.map(p => (p, SHA1.digest(p.file))),
    1.43 -                session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
    1.44 +                session_graph = thy_deps.session_graph(info.parent getOrElse "", imports_base))
    1.45  
    1.46              session_bases + (session_name -> base)
    1.47            }
    1.48 @@ -225,11 +224,9 @@
    1.49            }
    1.50        })
    1.51  
    1.52 -    val known =
    1.53 +    Deps(session_bases,
    1.54        if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
    1.55 -      else Known.empty
    1.56 -
    1.57 -    Deps(session_bases, known)
    1.58 +      else Known.empty)
    1.59    }
    1.60  
    1.61    def session_base(