# HG changeset patch
# User wenzelm
# Date 1491573186 -7200
# Node ID f8dd71a0791a06be2a60ebd75a1ef168e5ce4374
# Parent  7689342a3097f5f26f3e07da6750efaf2ac05903
support for all_known_theories of all sessions;

diff -r 7689342a3097 -r f8dd71a0791a src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Apr 07 15:35:00 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Apr 07 15:53:06 2017 +0200
@@ -66,6 +66,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,
@@ -163,13 +166,22 @@
     }))
   }
 
-  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(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)
   }