# HG changeset patch
# User wenzelm
# Date 1605565663 -3600
# Node ID 8d83acc5062e5978f1e3ac02edb2ef16f7b11f06
# Parent  5a616815cc44d9ef5314fc3b7749c4089f0315c8
clarified signature;

diff -r 5a616815cc44 -r 8d83acc5062e src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Pure/ML/ml_console.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -72,7 +72,7 @@
           session_base =
             if (raw_ml_system) None
             else Some(Sessions.base_info(
-              options, logic, dirs = dirs, include_sessions = include_sessions).check_base))
+              options, logic, dirs = dirs, include_sessions = include_sessions).check.base))
 
       POSIX_Interrupt.handler { process.interrupt } {
         new TTY_Loop(process.stdin, process.stdout).join
diff -r 5a616815cc44 -r 8d83acc5062e src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -558,7 +558,7 @@
       val session_base_info: Sessions.Base_Info,
       log: Logger = No_Logger)
     extends isabelle.Resources(
-      session_base_info.sessions_structure, session_base_info.check_base, log = log)
+      session_base_info.sessions_structure, session_base_info.check.base, log = log)
   {
     resources =>
 
diff -r 5a616815cc44 -r 8d83acc5062e src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Pure/Thy/sessions.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -357,7 +357,7 @@
     base: Base,
     infos: List[Info])
   {
-    def check_base: Base = if (errors.isEmpty) base else error(cat_lines(errors))
+    def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
   }
 
   def base_info(options: Options,
diff -r 5a616815cc44 -r 8d83acc5062e src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Pure/Tools/server_commands.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -73,8 +73,7 @@
 
       val base_info =
         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
-          include_sessions = args.include_sessions)
-      val base = base_info.check_base
+          include_sessions = args.include_sessions).check
 
       val results =
         Build.build(options,
diff -r 5a616815cc44 -r 8d83acc5062e src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -20,7 +20,7 @@
   def build_grammar(options: Options, progress: Progress = new Progress)
   {
     val logic = Grammar.default_logic
-    val keywords = Sessions.base_info(options, logic).check_base.overall_syntax.keywords
+    val keywords = Sessions.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 5a616815cc44 -r 8d83acc5062e src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -158,7 +158,7 @@
     if (more_args.nonEmpty) getopts.usage()
 
     val keywords =
-      Sessions.base_info(Options.init(), logic, dirs = dirs).check_base.overall_syntax.keywords
+      Sessions.base_info(Options.init(), logic, dirs = dirs).check.base.overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)
diff -r 5a616815cc44 -r 8d83acc5062e src/Tools/VSCode/src/server.scala
--- a/src/Tools/VSCode/src/server.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Tools/VSCode/src/server.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -264,9 +264,7 @@
         val base_info =
           Sessions.base_info(
             options, session_name, dirs = session_dirs, include_sessions = include_sessions,
-            session_ancestor = session_ancestor, session_requirements = session_requirements)
-
-        base_info.check_base
+            session_ancestor = session_ancestor, session_requirements = session_requirements).check
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options,
diff -r 5a616815cc44 -r 8d83acc5062e src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 16 23:19:07 2020 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Mon Nov 16 23:27:43 2020 +0100
@@ -73,7 +73,7 @@
     val options: Options,
     session_base_info: Sessions.Base_Info,
     log: Logger = No_Logger)
-  extends Resources(session_base_info.sessions_structure, session_base_info.check_base, log = log)
+  extends Resources(session_base_info.sessions_structure, session_base_info.check.base, log = log)
 {
   resources =>