# HG changeset patch
# User wenzelm
# Date 1660995317 -7200
# Node ID 423021c985006ff8c915a15a36f0698ae837c03d
# Parent  27bf2533f4a4a9bb3e163ed935fb42db6935a7f2
clarified signature: Sessions.Base_Info follows Sessions.Base;

diff -r 27bf2533f4a4 -r 423021c98500 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Sat Aug 20 13:35:17 2022 +0200
@@ -565,11 +565,12 @@
       print_mode: List[String] = Nil,
       progress: Progress = new Progress
     ): Session = {
-      val session = new Session(session_base_info.session, options, resources)
+      val session_name = session_base_info.session_name
+      val session = new Session(session_name, options, resources)
 
-      progress.echo("Starting session " + session_base_info.session + " ...")
+      progress.echo("Starting session " + session_name + " ...")
       Isabelle_Process.start(session, options, session_base_info.sessions_structure, store,
-        logic = session_base_info.session, modes = print_mode).await_startup()
+        logic = session_name, modes = print_mode).await_startup()
 
       session
     }
diff -r 27bf2533f4a4 -r 423021c98500 src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/Thy/export.scala	Sat Aug 20 13:35:17 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_errors.base.session_name
+      val session_name = session_base_info.check_errors.session_name
       val session_hierarchy = session_base_info.sessions_structure.build_hierarchy(session_name)
       val session_databases =
         database_server match {
diff -r 27bf2533f4a4 -r 423021c98500 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Sat Aug 20 13:35:17 2022 +0200
@@ -364,7 +364,7 @@
     errors: List[String] = Nil,
     infos: List[Info] = Nil
   ) {
-    def session: String = base.session_name
+    def session_name: String = base.session_name
 
     def check_errors: Base_Info =
       if (errors.isEmpty) this
diff -r 27bf2533f4a4 -r 423021c98500 src/Tools/VSCode/src/language_server.scala
--- a/src/Tools/VSCode/src/language_server.scala	Sat Aug 20 13:28:31 2022 +0200
+++ b/src/Tools/VSCode/src/language_server.scala	Sat Aug 20 13:35:17 2022 +0200
@@ -267,11 +267,11 @@
 
         def build(no_build: Boolean = false): Build.Results =
           Build.build(options,
-            selection = Sessions.Selection.session(base_info.session), build_heap = true,
-            no_build = no_build, dirs = session_dirs, infos = base_info.infos)
+            selection = Sessions.Selection.session(base_info.session_name),
+            build_heap = true, no_build = no_build, dirs = session_dirs, infos = base_info.infos)
 
         if (!session_no_build && !build(no_build = true).ok) {
-          val start_msg = "Build started for Isabelle/" + base_info.session + " ..."
+          val start_msg = "Build started for Isabelle/" + base_info.session_name + " ..."
           val fail_msg = "Session build failed -- prover process remains inactive!"
 
           val progress = channel.progress(verbose = true)
@@ -304,8 +304,8 @@
 
       try {
         Isabelle_Process.start(session, options, base_info.sessions_structure,
-          Sessions.store(options), modes = modes, logic = base_info.session).await_startup()
-        reply_ok("Welcome to Isabelle/" + base_info.session + Isabelle_System.isabelle_heading())
+          Sessions.store(options), modes = modes, logic = base_info.session_name).await_startup()
+        reply_ok("Welcome to Isabelle/" + base_info.session_name + Isabelle_System.isabelle_heading())
       }
       catch { case ERROR(msg) => reply_error(msg) }
     }