# HG changeset patch
# User wenzelm
# Date 1660994911 -7200
# Node ID 27bf2533f4a4a9bb3e163ed935fb42db6935a7f2
# Parent  ccb13acd52833f5c14e14146a53e7edc2a51bbf8
clarified signature: follow Sessions.Deps.check_errors (despite Process_Result.check);

diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/ML/ml_console.scala
--- a/src/Pure/ML/ml_console.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/ML/ml_console.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -70,7 +70,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_errors.base))
 
       POSIX_Interrupt.handler { process.interrupt() } {
         new TTY_Loop(process.stdin, process.stdout).join()
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/ML/ml_process.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -173,7 +173,7 @@
       val more_args = getopts(args)
       if (args.isEmpty || more_args.nonEmpty) getopts.usage()
 
-      val base_info = Sessions.base_info(options, logic, dirs = dirs).check
+      val base_info = Sessions.base_info(options, logic, dirs = dirs).check_errors
       val store = Sessions.store(options)
       val result =
         ML_Process(options, base_info.sessions_structure, store, logic = logic, args = eval_args,
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -549,7 +549,11 @@
       val options: Options,
       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) {
+    extends isabelle.Resources(
+      session_base_info.sessions_structure,
+      session_base_info.check_errors.base,
+      log = log
+    ) {
     resources =>
 
     val store: Sessions.Store = Sessions.store(options)
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -294,7 +294,7 @@
       document_snapshot: Option[Document.Snapshot] = None,
       close_database_context: Boolean = false
     ): Session_Context = {
-      val session_name = session_base_info.check.base.session_name
+      val session_name = session_base_info.check_errors.base.session_name
       val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
       val session_databases =
         database_server match {
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -364,8 +364,11 @@
     errors: List[String] = Nil,
     infos: List[Info] = Nil
   ) {
-    def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
     def session: String = base.session_name
+
+    def check_errors: Base_Info =
+      if (errors.isEmpty) this
+      else error(cat_lines(errors))
   }
 
   def base_info0(session: String): Base_Info =
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Pure/Tools/server_commands.scala
--- a/src/Pure/Tools/server_commands.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Pure/Tools/server_commands.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -68,7 +68,7 @@
 
       val base_info =
         Sessions.base_info(options, args.session, progress = progress, dirs = dirs,
-          include_sessions = args.include_sessions).check
+          include_sessions = args.include_sessions).check_errors
 
       val results =
         Build.build(options,
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Tools/VSCode/src/build_vscode_extension.scala
--- a/src/Tools/VSCode/src/build_vscode_extension.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Tools/VSCode/src/build_vscode_extension.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -21,7 +21,7 @@
     progress: Progress = new Progress
   ): Unit = {
     val keywords =
-      Sessions.base_info(options, logic, dirs = dirs).check.base.overall_syntax.keywords
+      Sessions.base_info(options, logic, dirs = dirs).check_errors.base.overall_syntax.keywords
 
     val output_path = build_dir + Path.explode("isabelle-grammar.json")
     progress.echo(output_path.expand.implode)
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -263,7 +263,7 @@
           Sessions.base_info(
             options, session_name, dirs = session_dirs,
             include_sessions = include_sessions, session_ancestor = session_ancestor,
-            session_requirements = session_requirements).check
+            session_requirements = session_requirements).check_errors
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options,
diff -r ccb13acd5283 -r 27bf2533f4a4 src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Sat Aug 20 13:16:15 2022 +0200
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Sat Aug 20 13:28:31 2022 +0200
@@ -71,7 +71,11 @@
   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_errors.base,
+  log = log
+) {
   resources =>
 
   private val state = Synchronized(VSCode_Resources.State())