# HG changeset patch
# User wenzelm
# Date 1504199174 -7200
# Node ID 191048506504268d619b56e9578b7a4bacb5c9df
# Parent  e16b27bd3f76f0e76f67f08e40373a3079045cbe
clarified signature: provide all_known information uniformly (it is subject to Sessions.T selection);

diff -r e16b27bd3f76 -r 191048506504 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 31 17:31:56 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 31 19:06:14 2017 +0200
@@ -153,8 +153,7 @@
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
-      global_theories: Map[String, String] = Map.empty,
-      all_known: Boolean = false): Deps =
+      global_theories: Map[String, String] = Map.empty): Deps =
   {
     val session_bases =
       (Map.empty[String, Base] /: sessions.imports_topological_order)({
@@ -274,9 +273,7 @@
           }
       })
 
-    Deps(session_bases,
-      if (all_known) Known.make(Path.current, session_bases.toList.map(_._2), Nil)
-      else Known.empty)
+    Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2), Nil))
   }
 
   def session_base_errors(
@@ -287,18 +284,12 @@
   {
     val full_sessions = load(options, dirs = dirs)
     val global_theories = full_sessions.global_theories
-    val selected_sessions = full_sessions.selection(Selection(sessions = List(session)))._2
+    val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
-    if (all_known) {
-      val deps =
-        Sessions.deps(full_sessions, global_theories = global_theories, all_known = all_known)
-      (deps.errors, deps(session).copy(known = deps.all_known))
-    }
-    else {
-      val deps =
-        Sessions.deps(selected_sessions, global_theories = global_theories)
-      (deps.errors, deps(session))
-    }
+    val sessions: T = if (all_known) full_sessions else selected_sessions
+    val deps = Sessions.deps(sessions, global_theories = global_theories)
+    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
+    (deps.errors, base)
   }
 
   def session_base(
diff -r e16b27bd3f76 -r 191048506504 src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Thu Aug 31 17:31:56 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Thu Aug 31 19:06:14 2017 +0200
@@ -87,8 +87,7 @@
 
     val deps =
       Sessions.deps(selected_sessions, progress = progress, verbose = verbose,
-        global_theories = full_sessions.global_theories,
-        all_known = true).check_errors
+        global_theories = full_sessions.global_theories).check_errors
 
     val root_keywords = Sessions.root_syntax.keywords