# HG changeset patch
# User wenzelm
# Date 1509471933 -3600
# Node ID 9f2de457b95e2c9e9e6f03ec42ad71b0cd177f46
# Parent  1c3d0c12bb5192333cab7c0ba521f413e79c301e
clarified signature;

diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/ML/ml_console.scala	Tue Oct 31 18:45:33 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_info(options, logic, dirs).check))
+            else Some(Sessions.session_base_info(options, logic, dirs).check_base))
       val process_output = Future.thread[Unit]("process_output") {
         try {
           var result = new StringBuilder(100)
diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Oct 31 18:45:33 2017 +0100
@@ -321,12 +321,6 @@
 
   /* 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,
@@ -338,13 +332,19 @@
     val global_theories = full_sessions.global_theories
     val (_, selected_sessions) = full_sessions.selection(Selection(sessions = List(session)))
 
-    val deps =
-      Sessions.deps(if (all_known) full_sessions else selected_sessions,
-        global_theories, inlined_files = inlined_files)
-
+    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)
 
-    Base_Info(base, deps.errors)
+    new Base_Info(sessions, deps, base)
+  }
+
+  final class Base_Info private [Sessions](val sessions: T, val deps: Deps, val base: Base)
+  {
+    def platform_path: Base_Info = new Base_Info(sessions, deps, base.platform_path)
+
+    def errors: List[String] = deps.errors
+    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
   }
 
 
diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Tue Oct 31 18:45:33 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_info(options, logic).check.overall_syntax.keywords
+    val keywords = Sessions.session_base_info(options, logic).check_base.overall_syntax.keywords
 
     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
     progress.echo(output_path.implode)
diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Tue Oct 31 18:45:33 2017 +0100
@@ -158,7 +158,7 @@
     if (more_args.nonEmpty) getopts.usage()
 
     val keywords =
-      Sessions.session_base_info(Options.init(), logic, dirs).check.overall_syntax.keywords
+      Sessions.session_base_info(Options.init(), logic, dirs).check_base.overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)
diff -r 1c3d0c12bb51 -r 9f2de457b95e src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Tue Oct 31 17:56:28 2017 +0100
+++ b/src/Tools/VSCode/src/server.scala	Tue Oct 31 18:45:33 2017 +0100
@@ -270,7 +270,7 @@
 
         val session_base =
           Sessions.session_base_info(
-            options, session_name, dirs = session_dirs, all_known = all_known).check
+            options, session_name, dirs = session_dirs, all_known = all_known).check_base
         val resources = new VSCode_Resources(options, session_base, log)
           {
             override def commit(change: Session.Change): Unit =