# HG changeset patch
# User wenzelm
# Date 1491589501 -7200
# Node ID d938705819bb7cc07c51f54024639f8c02eec264
# Parent  4a3e6cda3b94fc30c480be4f2e9e8888ae6d562a
tuned;

diff -r 4a3e6cda3b94 -r d938705819bb src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 19:35:39 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 20:25:01 2017 +0200
@@ -57,6 +57,10 @@
   {
     def loaded_theory(name: Document.Node.Name): Boolean =
       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])
@@ -110,12 +114,6 @@
             }
           }
 
-          val known_theories =
-            Base.known_theories(
-              parent_base :: info.imports.map(sessions(_)), thy_deps.deps.map(_.name))
-
-          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))
@@ -147,9 +145,11 @@
 
           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))
diff -r 4a3e6cda3b94 -r d938705819bb src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Apr 07 19:35:39 2017 +0200
+++ b/src/Pure/Tools/build.scala	Fri Apr 07 20:25:01 2017 +0200
@@ -197,10 +197,6 @@
       Future.thread("build") {
         val parent = info.parent.getOrElse("")
 
-        val known_theories =
-          for ((theory, node_name) <- deps(name).known_theories.toList)
-            yield (theory, node_name.node)
-
         val args_yxml =
           YXML.string_of_body(
             {
@@ -214,7 +210,7 @@
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
                 (info.theories,
-                known_theories)))))))))))))
+                deps(name).dest_known_theories)))))))))))))
             })
 
         val env =
diff -r 4a3e6cda3b94 -r d938705819bb src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Fri Apr 07 19:35:39 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Fri Apr 07 20:25:01 2017 +0200
@@ -95,13 +95,10 @@
       session_base match {
         case None => Nil
         case Some(base) =>
-          val known_theories =
-            for ((theory, node_name) <- base.known_theories.toList)
-              yield (theory, node_name.node)
           List("Resources.set_session_base {known_theories = " +
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
-                ML_Syntax.print_string, ML_Syntax.print_string))(known_theories) + "}")
+                ML_Syntax.print_string, ML_Syntax.print_string))(base.dest_known_theories) + "}")
       }
 
     // process