clarified signature;

--- a/src/Pure/ML/ml_console.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Pure/ML/ml_console.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -75,7 +75,7 @@
           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)))
+            else Some(Sessions.session_base_info(options, logic, dirs).check))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)

--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -318,34 +318,33 @@
     Deps(session_bases, Known.make(Path.current, session_bases.toList.map(_._2)))
   }
 
-  def session_base_errors(
+
+  /* base info */
+
+  sealed case class Base_Info(base: Base, errors: List[String])
+  {
+    def platform_path: Base_Info = copy(base = base.platform_path)
+    def check: Base = if (errors.isEmpty) base else error(cat_lines(errors))
+  }
+
+  def session_base_info(
     options: Options,
     session: String,
     dirs: List[Path] = Nil,
     inlined_files: Boolean = false,
-    all_known: Boolean = false): (List[String], Base) =
+    all_known: Boolean = false): Base_Info =
   {
     val full_sessions = load(options, dirs = dirs)
     val global_theories = full_sessions.global_theories
     val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
-    val sessions: T = if (all_known) full_sessions else selected_sessions
-    val deps = Sessions.deps(sessions, global_theories, inlined_files = inlined_files)
-    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
-    (deps.errors, base)
-  }
+    val deps =
+      Sessions.deps(if (all_known) full_sessions else selected_sessions,
+        global_theories, inlined_files = inlined_files)
 
-  def session_base(
-    options: Options,
-    session: String,
-    dirs: List[Path] = Nil,
-    inlined_files: Boolean = false,
-    all_known: Boolean = false): Base =
-  {
-    val (errs, base) =
-      session_base_errors(options, session, dirs = dirs,
-        inlined_files = inlined_files, all_known = all_known)
-    if (errs.isEmpty) base else error(cat_lines(errs))
+    val base = if (all_known) deps(session).copy(known = deps.all_known) else deps(session)
+
+    Base_Info(base, deps.errors)
   }
 
 

--- a/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -20,7 +20,7 @@
   def build_grammar(options: Options, progress: Progress = No_Progress)
   {
     val logic = Grammar.default_logic
-    val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
+    val keywords = Sessions.session_base_info(options, logic).check.overall_syntax.keywords
 
     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
     progress.echo(output_path.implode)

--- a/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -157,7 +157,8 @@
     val more_args = getopts(args)
     if (more_args.nonEmpty) getopts.usage()
 
-    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
+    val keywords =
+      Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)

--- a/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -269,7 +269,8 @@
         }
 
         val session_base =
-          Sessions.session_base(options, session_name, dirs = session_dirs, all_known = all_known)
+          Sessions.session_base_info(
+            options, session_name, dirs = session_dirs, all_known = all_known).check
         val resources = new VSCode_Resources(options, session_base, log)
           {
             override def commit(change: Session.Change): Unit =

--- a/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -24,15 +24,15 @@
 object JEdit_Resources
 {
   def apply(options: Options): JEdit_Resources =
-  {
-    val (errs, base) = JEdit_Sessions.session_base(options)
-    new JEdit_Resources(errs, base)
-  }
+    new JEdit_Resources(JEdit_Sessions.session_base_info(options))
 }
 
-class JEdit_Resources private(val session_errors: List[String], session_base: Sessions.Base)
-  extends Resources(session_base)
+class JEdit_Resources private(session_base_info: Sessions.Base_Info)
+  extends Resources(session_base_info.base)
 {
+  def session_errors: List[String] = session_base_info.errors
+
+
   /* document node name */
 
   def known_file(path: String): Option[Document.Node.Name] =

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 17:15:49 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Oct 31 17:56:28 2017 +0100
@@ -49,12 +49,12 @@
 
   def session_name(options: Options): String = session_info(options).name
 
-  def session_base(options: Options): (List[String], Sessions.Base) =
+  def session_base_info(options: Options): Sessions.Base_Info =
   {
-    val (errs, base) =
-      Sessions.session_base_errors(
-        options, session_name(options), dirs = JEdit_Sessions.session_dirs(), all_known = true)
-    (errs, base.platform_path)
+    Sessions.session_base_info(options,
+      session_name(options),
+      dirs = JEdit_Sessions.session_dirs(),
+      all_known = true).platform_path
   }
 
   def session_build_mode(): String = Isabelle_System.getenv("JEDIT_BUILD_MODE")