# HG changeset patch
# User wenzelm
# Date 1659607258 -7200
# Node ID 2eee2fdfb6e2d774973ed2811da6e2bf9cfa3c51
# Parent  45fc58d48e4a459cf3320c13f856b8461a0d7ca8
clarified signature: proper session_name for Sessions.Base (like Sessions.Info);

diff -r 45fc58d48e4a -r 2eee2fdfb6e2 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Thu Aug 04 11:29:40 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Thu Aug 04 12:00:58 2022 +0200
@@ -34,6 +34,8 @@
 ) {
   resources =>
 
+  def session_name: String = session_base.session_name
+
 
   /* init session */
 
diff -r 45fc58d48e4a -r 2eee2fdfb6e2 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 04 11:29:40 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Thu Aug 04 12:00:58 2022 +0200
@@ -59,6 +59,7 @@
   /* base info and source dependencies */
 
   sealed case class Base(
+    session_name: String = "",
     session_pos: Position.T = Position.none,
     session_directories: Map[JFile, String] = Map.empty,
     global_theories: Map[String, String] = Map.empty,
@@ -76,7 +77,8 @@
     errors: List[String] = Nil
   ) {
     override def toString: String =
-      "Sessions.Base(loaded_theories = " + loaded_theories.size +
+      "Sessions.Base(session_name = " + quote(session_name) +
+        ", loaded_theories = " + loaded_theories.size +
         ", used_theories = " + used_theories.length + ")"
 
     def theory_qualifier(name: String): String =
@@ -151,8 +153,13 @@
       }
     }
 
+    val bootstrap_bases = {
+      val base = sessions_structure.bootstrap
+      Map(base.session_name -> base)
+    }
+
     val session_bases =
-      sessions_structure.imports_topological_order.foldLeft(Map("" -> sessions_structure.bootstrap)) {
+      sessions_structure.imports_topological_order.foldLeft(bootstrap_bases) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
@@ -324,6 +331,7 @@
 
             val base =
               Base(
+                session_name = info.name,
                 session_pos = info.pos,
                 session_directories = sessions_structure.session_directories,
                 global_theories = sessions_structure.global_theories,
@@ -358,13 +366,13 @@
   /* base info */
 
   sealed case class Base_Info(
-    session: String,
     sessions_structure: Structure,
     errors: List[String],
     base: Base,
     infos: List[Info]
   ) {
     def check: Base_Info = if (errors.isEmpty) this else error(cat_lines(errors))
+    def session: String = base.session_name
   }
 
   def base_info(options: Options,
@@ -442,7 +450,7 @@
 
     val deps1 = Sessions.deps(selected_sessions1, progress = progress)
 
-    Base_Info(session1, full_sessions1, deps1.errors, deps1(session1), infos1)
+    Base_Info(full_sessions1, deps1.errors, deps1(session1), infos1)
   }
 
 
diff -r 45fc58d48e4a -r 2eee2fdfb6e2 src/Tools/jEdit/src/jedit_resources.scala
--- a/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 04 11:29:40 2022 +0200
+++ b/src/Tools/jEdit/src/jedit_resources.scala	Thu Aug 04 12:00:58 2022 +0200
@@ -28,7 +28,6 @@
 
 class JEdit_Resources private(val session_base_info: Sessions.Base_Info)
 extends Resources(session_base_info.sessions_structure, session_base_info.base) {
-  def session_name: String = session_base_info.session
   def session_errors: List[String] = session_base_info.errors