# HG changeset patch
# User wenzelm
# Date 1491592027 -7200
# Node ID e62b1af601f04fe83eb5680e453749cdcd7bd8ad
# Parent  c821f1f3d92d79aa4301a642d016ab1461bfecc9# Parent  a260181505c1db3936874c11f16160f530f72d50
merged

diff -r c821f1f3d92d -r e62b1af601f0 Admin/jenkins/build/ci_build_benchmark.scala
--- a/Admin/jenkins/build/ci_build_benchmark.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_benchmark.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -12,7 +12,6 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(sessions: Sessions.T) =
-    sessions.selection(session_groups = List("timing"))
+  def selection = Sessions.Selection(session_groups = List("timing"))
 
 }
diff -r c821f1f3d92d -r e62b1af601f0 Admin/jenkins/build/ci_build_makeall.scala
--- a/Admin/jenkins/build/ci_build_makeall.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -11,7 +11,6 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(sessions: Sessions.T) =
-    sessions.selection(all_sessions = true)
+  def selection = Sessions.Selection(all_sessions = true)
 
 }
diff -r c821f1f3d92d -r e62b1af601f0 Admin/jenkins/build/ci_build_makeall_seq.scala
--- a/Admin/jenkins/build/ci_build_makeall_seq.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/Admin/jenkins/build/ci_build_makeall_seq.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -11,7 +11,6 @@
   def pre_hook(args: List[String]) = {}
   def post_hook(results: Build.Results) = {}
 
-  def select_sessions(sessions: Sessions.T) =
-    sessions.selection(all_sessions = true)
+  def selection = Sessions.Selection(all_sessions = true)
 
 }
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Admin/build_doc.scala
--- a/src/Pure/Admin/build_doc.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Admin/build_doc.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -24,7 +24,7 @@
   {
     val selection =
       for {
-        (name, info) <- Sessions.load(options).topological_order
+        (name, info) <- Sessions.load(options).build_topological_order
         if info.groups.contains("doc")
         doc = info.options.string("document_variants")
         if all_docs || docs.contains(doc)
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Admin/ci_profile.scala
--- a/src/Pure/Admin/ci_profile.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Admin/ci_profile.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -19,7 +19,7 @@
     val progress = new Console_Progress(verbose = true)
     val start_time = Time.now()
     val results = progress.interrupt_handler {
-      Build.build_selection(
+      Build.build(
         options = options,
         progress = progress,
         clean_build = clean,
@@ -28,7 +28,7 @@
         dirs = include,
         select_dirs = select,
         system_mode = true,
-        selection = select_sessions _)
+        selection = selection)
     }
     val end_time = Time.now()
     (results, end_time - start_time)
@@ -146,5 +146,5 @@
   def pre_hook(args: List[String]): Unit
   def post_hook(results: Build.Results): Unit
 
-  def select_sessions(sessions: Sessions.T): (List[String], Sessions.T)
+  def selection: Sessions.Selection
 }
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/ML/ml_syntax.scala
--- a/src/Pure/ML/ml_syntax.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/ML/ml_syntax.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -46,6 +46,12 @@
     quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
 
 
+  /* pair */
+
+  def print_pair[A, B](f: A => String, g: B => String)(pair: (A, B)): String =
+    "(" + f(pair._1) + ", " + g(pair._2) + ")"
+
+
   /* list */
 
   def print_list[A](f: A => String)(list: List[A]): String =
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Apr 07 21:07:07 2017 +0200
@@ -6,6 +6,9 @@
 
 signature RESOURCES =
 sig
+  val set_session_base: {known_theories: (string * string) list} -> unit
+  val reset_session_base: unit -> unit
+  val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val thy_path: Path.T -> Path.T
@@ -25,6 +28,23 @@
 structure Resources: RESOURCES =
 struct
 
+(* session base *)
+
+val global_session_base =
+  Synchronized.var "Sessions.base"
+    ({known_theories = Symtab.empty: Path.T Symtab.table});
+
+fun set_session_base {known_theories} =
+  Synchronized.change global_session_base
+    (K {known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
+
+fun reset_session_base () =
+  set_session_base {known_theories = []};
+
+fun known_theory name =
+  Symtab.lookup (#known_theories (Synchronized.value global_session_base)) name;
+
+
 (* manage source files *)
 
 type files =
@@ -62,15 +82,20 @@
 
 fun check_thy dir thy_name =
   let
-    val path = thy_path (Path.basic thy_name);
-    val master_file = check_file dir path;
+    val thy_base_name = Long_Name.base_name thy_name;
+    val thy_path = thy_path (Path.basic thy_base_name);
+    val master_file =
+      (case known_theory thy_name of
+        NONE => check_file dir thy_path
+      | SOME known_path => check_file Path.current known_path);
     val text = File.read master_file;
 
     val {name = (name, pos), imports, keywords} =
       Thy_Header.read (Path.position master_file) text;
-    val _ = thy_name <> name andalso
-      error ("Bad theory name " ^ quote name ^
-        " for file " ^ Path.print path ^ Position.here pos);
+    val _ =
+      thy_base_name <> name andalso
+        error ("Bad theory name " ^ quote name ^
+          " for file " ^ Path.print thy_path ^ Position.here pos);
   in
    {master = (master_file, SHA1.digest text), text = text, theory_pos = pos,
     imports = imports, keywords = keywords}
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -74,15 +74,14 @@
       if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)) theory0
       else Long_Name.qualify(session_name, theory0)
 
-    session_base.known_theories.get(theory) orElse session_base.known_theories.get(theory0) match
-    {
-      case Some(name) if session_base.loaded_theory(name) => name.loaded_theory
-      case Some(name) => name
-      case None =>
-        val path = Path.explode(s)
-        val node = append(dir, thy_path(path))
-        val master_dir = append(dir, path.dir)
-        Document.Node.Name(node, master_dir, theory)
+    session_base.loaded_theories.get(theory) orElse
+    session_base.loaded_theories.get(theory0) orElse
+    session_base.known_theories.get(theory) orElse
+    session_base.known_theories.get(theory0) getOrElse {
+      val path = Path.explode(s)
+      val node = append(dir, thy_path(path))
+      val master_dir = append(dir, path.dir)
+      Document.Node.Name(node, master_dir, theory)
     }
   }
 
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -1,7 +1,7 @@
 /*  Title:      Pure/Thy/sessions.scala
     Author:     Makarius
 
-Isabelle session information.
+Cumulative session information.
 */
 
 package isabelle
@@ -27,11 +27,28 @@
 
     lazy val bootstrap: Base =
       Base(keywords = Thy_Header.bootstrap_header, syntax = Thy_Header.bootstrap_syntax)
+
+    private[Sessions] def known_theories(bases: Iterable[Base], names: Iterable[Document.Node.Name])
+      : Map[String, Document.Node.Name] =
+    {
+      val bases_iterator =
+        for { base <- bases.iterator; (_, name) <- base.known_theories.iterator }
+          yield name
+
+      (Map.empty[String, Document.Node.Name] /: (bases_iterator ++ names.iterator))({
+        case (known, name) =>
+          known.get(name.theory) match {
+            case Some(name1) if name != name1 =>
+              error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
+            case _ => known + (name.theory -> name)
+          }
+        })
+    }
   }
 
   sealed case class Base(
     global_theories: Set[String] = Set.empty,
-    loaded_theories: Set[String] = Set.empty,
+    loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -39,7 +56,11 @@
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph)
   {
     def loaded_theory(name: Document.Node.Name): Boolean =
-      loaded_theories.contains(name.theory)
+      loaded_theories.isDefinedAt(name.theory)
+
+    def dest_known_theories: List[(String, String)] =
+      for ((theory, node_name) <- known_theories.toList)
+        yield (theory, node_name.node)
   }
 
   sealed case class Deps(sessions: Map[String, Base])
@@ -47,6 +68,9 @@
     def is_empty: Boolean = sessions.isEmpty
     def apply(name: String): Base = sessions(name)
     def sources(name: String): List[SHA1.Digest] = sessions(name).sources.map(_._2)
+
+    def all_known_theories: Map[String, Document.Node.Name] =
+      Base.known_theories(sessions.toList.map(_._2), Nil)
   }
 
   def deps(sessions: T,
@@ -57,8 +81,8 @@
       check_keywords: Set[String] = Set.empty,
       global_theories: Set[String] = Set.empty): Deps =
   {
-    Deps((Map.empty[String, Base] /: sessions.topological_order)({
-      case (sessions, (name, info)) =>
+    Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
+      case (sessions, (session_name, info)) =>
         if (progress.stopped) throw Exn.Interrupt()
 
         try {
@@ -67,13 +91,13 @@
               case None => Base.bootstrap
               case Some(parent) => sessions(parent)
             }
-          val resources = new Resources(name, parent_base)
+          val resources = new Resources(session_name, parent_base)
 
           if (verbose || list_files) {
             val groups =
               if (info.groups.isEmpty) ""
               else info.groups.mkString(" (", " ", ")")
-            progress.echo("Session " + info.chapter + "/" + name + groups)
+            progress.echo("Session " + info.chapter + "/" + session_name + groups)
           }
 
           val thy_deps =
@@ -90,27 +114,13 @@
             }
           }
 
-          val known_theories =
-            (parent_base.known_theories /: thy_deps.deps)({ case (known, dep) =>
-              val name = dep.name
-              known.get(name.theory) match {
-                case Some(name1) if name != name1 =>
-                  error("Duplicate theory " + quote(name.node) + " vs. " + quote(name1.node))
-                case _ =>
-                  known + (name.theory -> name) +
-                    (Long_Name.base_name(name.theory) -> name)  // legacy
-              }
-            })
-
-          val loaded_theories = thy_deps.loaded_theories
-          val keywords = thy_deps.keywords
           val syntax = thy_deps.syntax
 
           val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
           val loaded_files =
             if (inlined_files) {
               val pure_files =
-                if (is_pure(name)) {
+                if (is_pure(session_name)) {
                   val roots = Thy_Header.ml_roots.map(p => info.dir + Path.explode(p._1))
                   val files =
                     roots.flatMap(root => resources.loaded_files(syntax, File.read(root))).
@@ -135,29 +145,41 @@
 
           val base =
             Base(global_theories = global_theories,
-              loaded_theories = loaded_theories,
-              known_theories = known_theories,
-              keywords = keywords,
+              loaded_theories = thy_deps.loaded_theories,
+              known_theories =
+                Base.known_theories(
+                  parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name)),
+              keywords = thy_deps.keywords,
               syntax = syntax,
               sources = all_files.map(p => (p, SHA1.digest(p.file))),
               session_graph = thy_deps.session_graph(info.parent getOrElse "", parent_base))
 
-          sessions + (name -> base)
+          sessions + (session_name -> base)
         }
         catch {
           case ERROR(msg) =>
             cat_error(msg, "The error(s) above occurred in session " +
-              quote(name) + Position.here(info.pos))
+              quote(session_name) + Position.here(info.pos))
         }
     }))
   }
 
-  def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
+  def session_base(
+    options: Options,
+    session: String,
+    dirs: List[Path] = Nil,
+    all_known_theories: Boolean = false): Base =
   {
     val full_sessions = load(options, dirs = dirs)
-    val (_, selected_sessions) = full_sessions.selection(sessions = List(session))
+    val global_theories = full_sessions.global_theories
+    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
 
-    deps(selected_sessions, global_theories = full_sessions.global_theories)(session)
+    if (all_known_theories) {
+      val deps = Sessions.deps(full_sessions, global_theories = global_theories)
+      deps(session).copy(known_theories = deps.all_known_theories)
+    }
+    else
+      deps(selected_sessions, global_theories = global_theories)(session)
   }
 
 
@@ -172,6 +194,7 @@
     parent: Option[String],
     description: String,
     options: Options,
+    imports: List[String],
     theories: List[(Options, List[String])],
     global_theories: List[String],
     files: List[Path],
@@ -181,62 +204,32 @@
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
   }
 
-  def make(infos: Traversable[(String, Info)]): T =
+  object Selection
   {
-    val graph1 =
-      (Graph.string[Info] /: infos) {
-        case (graph, (name, info)) =>
-          if (graph.defined(name))
-            error("Duplicate session " + quote(name) + Position.here(info.pos) +
-              Position.here(graph.get_node(name).pos))
-          else graph.new_node(name, info)
-      }
-    val graph2 =
-      (graph1 /: graph1.iterator) {
-        case (graph, (name, (info, _))) =>
-          info.parent match {
-            case None => graph
-            case Some(parent) =>
-              if (!graph.defined(parent))
-                error("Bad parent session " + quote(parent) + " for " +
-                  quote(name) + Position.here(info.pos))
-
-              try { graph.add_edge_acyclic(parent, name) }
-              catch {
-                case exn: Graph.Cycles[_] =>
-                  error(cat_lines(exn.cycles.map(cycle =>
-                    "Cyclic session dependency of " +
-                      cycle.map(c => quote(c.toString)).mkString(" via "))) +
-                        Position.here(info.pos))
-              }
-          }
-      }
-
-    new T(graph2)
+    val empty: Selection = Selection()
   }
 
-  final class T private[Sessions](val graph: Graph[String, Info])
-    extends PartialFunction[String, Info]
+  sealed case class Selection(
+    requirements: Boolean = false,
+    all_sessions: Boolean = false,
+    exclude_session_groups: List[String] = Nil,
+    exclude_sessions: List[String] = Nil,
+    session_groups: List[String] = Nil,
+    sessions: List[String] = Nil)
   {
-    def apply(name: String): Info = graph.get_node(name)
-    def isDefinedAt(name: String): Boolean = graph.defined(name)
+    def + (other: Selection): Selection =
+      Selection(
+        requirements = requirements || other.requirements,
+        all_sessions = all_sessions || other.all_sessions,
+        exclude_session_groups = exclude_session_groups ::: other.exclude_session_groups,
+        exclude_sessions = exclude_sessions ::: other.exclude_sessions,
+        session_groups = session_groups ::: other.session_groups,
+        sessions = sessions ::: other.sessions)
 
-    def global_theories: Set[String] =
-      (for {
-        (_, (info, _)) <- graph.iterator
-        name <- info.global_theories.iterator }
-       yield name).toSet
-
-    def selection(
-      requirements: Boolean = false,
-      all_sessions: Boolean = false,
-      exclude_session_groups: List[String] = Nil,
-      exclude_sessions: List[String] = Nil,
-      session_groups: List[String] = Nil,
-      sessions: List[String] = Nil): (List[String], T) =
+    def apply(graph: Graph[String, Info]): (List[String], Graph[String, Info]) =
     {
       val bad_sessions =
-        SortedSet((exclude_sessions ::: sessions).filterNot(isDefinedAt(_)): _*).toList
+        SortedSet((exclude_sessions ::: sessions).filterNot(graph.defined(_)): _*).toList
       if (bad_sessions.nonEmpty) error("Undefined session(s): " + commas_quote(bad_sessions))
 
       val excluded =
@@ -245,7 +238,7 @@
         val exclude_group_sessions =
           (for {
             (name, (info, _)) <- graph.iterator
-            if apply(name).groups.exists(exclude_group)
+            if graph.get_node(name).groups.exists(exclude_group)
           } yield name).toList
         graph.all_succs(exclude_group_sessions ::: exclude_sessions).toSet
       }
@@ -258,7 +251,7 @@
           val select = sessions.toSet
           (for {
             (name, (info, _)) <- graph.iterator
-            if info.select || select(name) || apply(name).groups.exists(select_group)
+            if info.select || select(name) || graph.get_node(name).groups.exists(select_group)
           } yield name).toList
         }
       }.filterNot(excluded)
@@ -267,17 +260,89 @@
         if (requirements) (graph.all_preds(pre_selected).toSet -- pre_selected).toList
         else pre_selected
 
-      val graph1 = graph.restrict(graph.all_preds(selected).toSet)
-      (selected, new T(graph1))
+      (selected, graph.restrict(graph.all_preds(selected).toSet))
+    }
+  }
+
+  def make(infos: Traversable[(String, Info)]): T =
+  {
+    def add_edges(graph: Graph[String, Info], kind: String, edges: Info => Traversable[String])
+      : Graph[String, Info] =
+    {
+      def add_edge(pos: Position.T, name: String, g: Graph[String, Info], parent: String) =
+      {
+        if (!g.defined(parent))
+          error("Bad " + kind + " session " + quote(parent) + " for " +
+            quote(name) + Position.here(pos))
+
+        try { g.add_edge_acyclic(parent, name) }
+        catch {
+          case exn: Graph.Cycles[_] =>
+            error(cat_lines(exn.cycles.map(cycle =>
+              "Cyclic session dependency of " +
+                cycle.map(c => quote(c.toString)).mkString(" via "))) + Position.here(pos))
+        }
+      }
+      (graph /: graph.iterator) {
+        case (g, (name, (info, _))) => (g /: edges(info))(add_edge(info.pos, name, _, _))
+      }
     }
 
-    def ancestors(name: String): List[String] =
-      graph.all_preds(List(name)).tail.reverse
+    val graph0 =
+      (Graph.string[Info] /: infos) {
+        case (graph, (name, info)) =>
+          if (graph.defined(name))
+            error("Duplicate session " + quote(name) + Position.here(info.pos) +
+              Position.here(graph.get_node(name).pos))
+          else graph.new_node(name, info)
+      }
+    val graph1 = add_edges(graph0, "parent", _.parent)
+    val graph2 = add_edges(graph1, "imports", _.imports)
+
+    new T(graph1, graph2)
+  }
+
+  final class T private[Sessions](
+      val build_graph: Graph[String, Info],
+      val imports_graph: Graph[String, Info])
+  {
+    def apply(name: String): Info = imports_graph.get_node(name)
+    def get(name: String): Option[Info] =
+      if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
-    def topological_order: List[(String, Info)] =
-      graph.topological_order.map(name => (name, apply(name)))
+    def global_theories: Set[String] =
+      (Set.empty[String] /:
+        (for {
+          (_, (info, _)) <- imports_graph.iterator
+          thy <- info.global_theories.iterator }
+         yield (thy, info.pos)))(
+          { case (set, (thy, pos)) =>
+             if (set.contains(thy))
+               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
+             else set + thy
+           })
 
-    override def toString: String = graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
+    def selection(select: Selection): (List[String], T) =
+    {
+      val (_, build_graph1) = select(build_graph)
+      val (selected, imports_graph1) = select(imports_graph)
+      (selected, new T(build_graph1, imports_graph1))
+    }
+
+    def build_ancestors(name: String): List[String] =
+      build_graph.all_preds(List(name)).tail.reverse
+
+    def build_descendants(names: List[String]): List[String] =
+      build_graph.all_succs(names)
+
+    def build_topological_order: List[(String, Info)] =
+      build_graph.topological_order.map(name => (name, apply(name)))
+
+    def imports_topological_order: List[(String, Info)] =
+      imports_graph.topological_order.map(name => (name, apply(name)))
+
+    override def toString: String =
+      imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")
   }
 
 
@@ -291,6 +356,7 @@
   private val IN = "in"
   private val DESCRIPTION = "description"
   private val OPTIONS = "options"
+  private val SESSIONS = "sessions"
   private val THEORIES = "theories"
   private val GLOBAL = "global"
   private val FILES = "files"
@@ -302,6 +368,7 @@
       (SESSION, Keyword.THY_DECL) +
       (DESCRIPTION, Keyword.QUASI_COMMAND) +
       (OPTIONS, Keyword.QUASI_COMMAND) +
+      (SESSIONS, Keyword.QUASI_COMMAND) +
       (THEORIES, Keyword.QUASI_COMMAND) +
       (FILES, Keyword.QUASI_COMMAND) +
       (DOCUMENT_FILES, Keyword.QUASI_COMMAND)
@@ -318,6 +385,7 @@
       parent: Option[String],
       description: String,
       options: List[Options.Spec],
+      imports: List[String],
       theories: List[(List[Options.Spec], List[(String, Boolean)])],
       files: List[String],
       document_files: List[(String, String)]) extends Entry
@@ -363,11 +431,12 @@
             (opt(session_name ~! $$$("+") ^^ { case x ~ _ => x }) ~
               (($$$(DESCRIPTION) ~! text ^^ { case _ ~ x => x }) | success("")) ~
               (($$$(OPTIONS) ~! options ^^ { case _ ~ x => x }) | success(Nil)) ~
+              (($$$(SESSIONS) ~! rep(session_name)  ^^ { case _ ~ x => x }) | success(Nil)) ~
               rep1(theories) ~
               (($$$(FILES) ~! rep1(path) ^^ { case _ ~ x => x }) | success(Nil)) ~
               (rep(document_files) ^^ (x => x.flatten))))) ^^
-        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i))) =>
-            Session_Entry(pos, a, b, c, d, e, f, g, h, i) }
+        { case _ ~ ((a, pos) ~ b ~ c ~ (_ ~ (d ~ e ~ f ~ g ~ h ~ i ~ j))) =>
+            Session_Entry(pos, a, b, c, d, e, f, g, h, i, j) }
     }
 
     def parse(options: Options, select: Boolean, dir: Path): List[(String, Info)] =
@@ -401,12 +470,12 @@
 
           val meta_digest =
             SHA1.digest((entry_chapter, name, entry.parent, entry.options,
-              entry.theories, entry.files, entry.document_files).toString)
+              entry.imports, entry.theories, entry.files, entry.document_files).toString)
 
           val info =
             Info(entry_chapter, select, entry.pos, entry.groups, dir + Path.explode(entry.path),
-              entry.parent, entry.description, session_options, theories, global_theories,
-              files, document_files, meta_digest)
+              entry.parent, entry.description, session_options, entry.imports, theories,
+              global_theories, files, document_files, meta_digest)
 
           (name, info)
         }
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -67,7 +67,7 @@
       val import_errors =
         (for {
           (theory, imports) <- seen_theory.iterator_list
-          if !resources.session_base.loaded_theories(theory)
+          if !resources.session_base.loaded_theories.isDefinedAt(theory)
           if imports.length > 1
         } yield {
           "Incoherent imports for theory " + quote(theory) + ":\n" +
@@ -80,11 +80,12 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Set[String] =
+    def loaded_theories: Map[String, Document.Node.Name] =
       (resources.session_base.loaded_theories /: rev_deps) {
         case (loaded, dep) =>
-          loaded + dep.name.theory +
-            Long_Name.base_name(dep.name.theory)  // legacy
+          val name = dep.name.loaded_theory
+          loaded + (name.theory -> name) +
+            (Long_Name.base_name(name.theory) -> name)  // legacy
       }
 
     def loaded_files: List[Path] =
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/build.ML	Fri Apr 07 21:07:07 2017 +0200
@@ -144,30 +144,37 @@
   chapter: string,
   name: string,
   master_dir: Path.T,
-  theories: (Options.T * (string * Position.T) list) list};
+  theories: (Options.T * (string * Position.T) list) list,
+  known_theories: (string * string) list};
 
 fun decode_args yxml =
   let
     open XML.Decode;
     val (symbol_codes, (command_timings, (do_output, (verbose, (browser_info,
-      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir, theories))))))))))) =
+      (document_files, (graph_file, (parent_name, (chapter, (name, (master_dir,
+      (theories, known_theories)))))))))))) =
       pair (list (pair string int)) (pair (list properties) (pair bool (pair bool (pair string
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
-          (pair string (((list (pair Options.decode (list (string #> rpair Position.none))))))))))))))))
+          (pair string
+            (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
+              (list (pair string string)))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
       verbose = verbose, browser_info = Path.explode browser_info,
       document_files = map (apply2 Path.explode) document_files,
       graph_file = Path.explode graph_file, parent_name = parent_name, chapter = chapter,
-      name = name, master_dir = Path.explode master_dir, theories = theories}
+      name = name, master_dir = Path.explode master_dir, theories = theories,
+      known_theories = known_theories}
   end;
 
 fun build_session (Args {symbol_codes, command_timings, do_output, verbose, browser_info,
-    document_files, graph_file, parent_name, chapter, name, master_dir, theories}) =
+    document_files, graph_file, parent_name, chapter, name, master_dir, theories, known_theories}) =
   let
     val symbols = HTML.make_symbols symbol_codes;
 
+    val _ = Resources.set_session_base {known_theories = known_theories};
+
     val _ =
       Session.init
         symbols
@@ -191,6 +198,8 @@
           |> session_timing name verbose
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
+
+    val _ = Resources.reset_session_base ();
     val _ = Par_Exn.release_all [res1, res2];
   in () end;
 
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -65,7 +65,7 @@
 
     def apply(sessions: Sessions.T, store: Sessions.Store): Queue =
     {
-      val graph = sessions.graph
+      val graph = sessions.build_graph
       val names = graph.keys
 
       val timings = names.map(name => (name, load_timings(store, name)))
@@ -204,11 +204,13 @@
               pair(list(pair(string, int)), pair(list(properties), pair(bool, pair(bool,
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
-                list(pair(Options.encode, list(string))))))))))))))(
+                pair(list(pair(Options.encode, list(string))),
+                list(pair(string, string))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
-                info.theories))))))))))))
+                (info.theories,
+                deps(name).dest_known_theories)))))))))))))
             })
 
         val env =
@@ -351,51 +353,20 @@
     exclude_session_groups: List[String] = Nil,
     exclude_sessions: List[String] = Nil,
     session_groups: List[String] = Nil,
-    sessions: List[String] = Nil): Results =
-  {
-    build_selection(
-      options = options,
-      progress = progress,
-      build_heap = build_heap,
-      clean_build = clean_build,
-      dirs = dirs,
-      select_dirs = select_dirs,
-      numa_shuffling = numa_shuffling,
-      max_jobs = max_jobs,
-      list_files = list_files,
-      check_keywords = check_keywords,
-      no_build = no_build,
-      system_mode = system_mode,
-      verbose = verbose,
-      pide = pide,
-      selection = { full_sessions =>
-        full_sessions.selection(requirements, all_sessions,
-          exclude_session_groups, exclude_sessions, session_groups, sessions) })
-  }
-
-  def build_selection(
-      options: Options,
-      progress: Progress = No_Progress,
-      build_heap: Boolean = false,
-      clean_build: Boolean = false,
-      dirs: List[Path] = Nil,
-      select_dirs: List[Path] = Nil,
-      numa_shuffling: Boolean = false,
-      max_jobs: Int = 1,
-      list_files: Boolean = false,
-      check_keywords: Set[String] = Set.empty,
-      no_build: Boolean = false,
-      system_mode: Boolean = false,
-      verbose: Boolean = false,
-      pide: Boolean = false,
-      selection: Sessions.T => (List[String], Sessions.T) = (_.selection(all_sessions = true))
-    ): Results =
+    sessions: List[String] = Nil,
+    selection: Sessions.Selection = Sessions.Selection.empty): Results =
   {
     /* session selection and dependencies */
 
     val build_options = options.int.update("completion_limit", 0).bool.update("ML_statistics", true)
+
     val full_sessions = Sessions.load(build_options, dirs, select_dirs)
-    val (selected, selected_sessions) = selection(full_sessions)
+
+    val (selected, selected_sessions) =
+      full_sessions.selection(
+          Sessions.Selection(requirements, all_sessions, exclude_session_groups,
+            exclude_sessions, session_groups, sessions) + selection)
+
     val deps =
       Sessions.deps(selected_sessions, progress = progress, inlined_files = true,
         verbose = verbose, list_files = list_files, check_keywords = check_keywords,
@@ -414,7 +385,7 @@
 
     // optional cleanup
     if (clean_build) {
-      for (name <- full_sessions.graph.all_succs(selected)) {
+      for (name <- full_sessions.build_descendants(selected)) {
         val files =
           List(Path.basic(name), store.database(name), store.log(name), store.log_gz(name)).
             map(store.output_dir + _).filter(_.is_file)
@@ -520,7 +491,7 @@
             //{{{ check/start next job
             pending.dequeue(running.isDefinedAt(_)) match {
               case Some((name, info)) =>
-                val ancestor_results = selected_sessions.ancestors(name).map(results(_))
+                val ancestor_results = selected_sessions.build_ancestors(name).map(results(_))
                 val ancestor_heaps = ancestor_results.flatMap(_.heap_stamp)
 
                 val do_output = build_heap || Sessions.is_pure(name) || queue.is_inner(name)
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Tools/ml_console.scala
--- a/src/Pure/Tools/ml_console.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/ml_console.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -72,7 +72,10 @@
       val process =
         ML_Process(options, logic = logic, args = List("-i"), dirs = dirs, redirect = true,
           modes = if (raw_ml_system) Nil else modes ::: List("ASCII"),
-          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode))
+          raw_ml_system = raw_ml_system, store = Sessions.store(system_mode),
+          session_base =
+            if (raw_ml_system) None
+            else Some(Sessions.session_base(options, logic, dirs)))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)
diff -r c821f1f3d92d -r e62b1af601f0 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -24,15 +24,17 @@
     cleanup: () => Unit = () => (),
     channel: Option[System_Channel] = None,
     sessions: Option[Sessions.T] = None,
+    session_base: Option[Sessions.Base] = None,
     store: Sessions.Store = Sessions.store()): Bash.Process =
   {
     val logic_name = Isabelle_System.default_logic(logic)
     val heaps: List[String] =
       if (raw_ml_system) Nil
       else {
+        val selection = Sessions.Selection(sessions = List(logic_name))
         val (_, selected_sessions) =
-          sessions.getOrElse(Sessions.load(options, dirs)).selection(sessions = List(logic_name))
-        (selected_sessions.ancestors(logic_name) ::: List(logic_name)).
+          sessions.getOrElse(Sessions.load(options, dirs)).selection(selection)
+        (selected_sessions.build_ancestors(logic_name) ::: List(logic_name)).
           map(a => File.platform_path(store.heap(a)))
       }
 
@@ -88,6 +90,18 @@
     val env_options = Map("ISABELLE_PROCESS_OPTIONS" -> File.standard_path(isabelle_process_options))
     val eval_options = if (heaps.isEmpty) Nil else List("Options.load_default ()")
 
+    // session base
+    val eval_session_base =
+      session_base match {
+        case None => Nil
+        case Some(base) =>
+          List("Resources.set_session_base {known_theories = " +
+            ML_Syntax.print_list(
+              ML_Syntax.print_pair(
+                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
+      }
+
+    // process
     val eval_process =
       if (heaps.isEmpty)
         List("PolyML.print_depth " + ML_Syntax.print_int(options.int("ML_print_depth")))
@@ -113,7 +127,7 @@
     // bash
     val bash_args =
       ml_runtime_options :::
-      (eval_init ::: eval_modes ::: eval_options ::: eval_process).
+      (eval_init ::: eval_modes ::: eval_options ::: eval_session_base ::: eval_process).
         map(eval => List("--eval", eval)).flatten ::: args
 
     Bash.process(
diff -r c821f1f3d92d -r e62b1af601f0 src/Tools/jEdit/src/jedit_sessions.scala
--- a/src/Tools/jEdit/src/jedit_sessions.scala	Fri Apr 07 10:56:41 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Fri Apr 07 21:07:07 2017 +0200
@@ -38,10 +38,10 @@
         options.string(option_name))
 
     (for {
-      tree <-
+      sessions <-
         try { Some(Sessions.load(session_options(options), dirs = session_dirs())) }
         catch { case ERROR(_) => None }
-      info <- tree.lift(logic)
+      info <- sessions.get(logic)
       parent <- info.parent
       if Isabelle_System.getenv("JEDIT_LOGIC_ROOT") == "true"
     } yield Info(parent, info.pos)) getOrElse Info(logic, Position.none)
@@ -75,9 +75,9 @@
 
   def session_list(options: Options): List[String] =
   {
-    val session_tree = Sessions.load(options, dirs = session_dirs())
+    val sessions = Sessions.load(options, dirs = session_dirs())
     val (main_sessions, other_sessions) =
-      session_tree.topological_order.partition(p => p._2.groups.contains("main"))
+      sessions.imports_topological_order.partition(p => p._2.groups.contains("main"))
     main_sessions.map(_._1).sorted ::: other_sessions.map(_._1).sorted
   }