# HG changeset patch
# User wenzelm
# Date 1660742297 -7200
# Node ID 8342cba8eae86ee9915a9eab96934154fdfb42f0
# Parent  3d8b37b1d798b160447c83806601e02e5da097cf
clarified signature: avoid constants from Sessions.Structure within Session.Base;

diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Wed Aug 17 14:42:20 2022 +0200
+++ b/src/Pure/ML/ml_process.scala	Wed Aug 17 15:18:17 2022 +0200
@@ -80,7 +80,7 @@
     // session base
     val (init_session_base, eval_init_session) =
       session_base match {
-        case None => (sessions_structure.bootstrap, Nil)
+        case None => (Sessions.bootstrap_base, Nil)
         case Some(base) => (base, List("Resources.init_session_env ()"))
       }
     val init_session = Isabelle_System.tmp_file("init_session")
diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Wed Aug 17 14:42:20 2022 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Aug 17 15:18:17 2022 +0200
@@ -57,7 +57,7 @@
        (command_timings,
        (Command_Span.load_commands.map(cmd => (cmd.name, cmd.position)),
        (Scala.functions,
-       (session_base.global_theories.toList,
+       (sessions_structure.global_theories.toList,
         session_base.loaded_theories.keys)))))))))
   }
 
@@ -150,9 +150,11 @@
     } yield file
   }
 
+  def global_theory(theory: String): Boolean =
+    sessions_structure.global_theories.isDefinedAt(theory)
+
   def theory_name(qualifier: String, theory: String): String =
-    if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
-      theory
+    if (Long_Name.is_qualified(theory) || global_theory(theory)) theory
     else Long_Name.qualify(qualifier, theory)
 
   def find_theory_node(theory: String): Option[Document.Node.Name] = {
@@ -189,7 +191,7 @@
 
   def find_theory(file: JFile): Option[Document.Node.Name] = {
     for {
-      qualifier <- session_base.session_directories.get(File.canonical(file).getParentFile)
+      qualifier <- sessions_structure.session_directories.get(File.canonical(file).getParentFile)
       theory_base <- proper_string(Thy_Header.theory_name(file.getName))
       theory = theory_name(qualifier, theory_base)
       theory_node <- find_theory_node(theory)
@@ -208,7 +210,7 @@
       theory <- Thy_Header.try_read_dir(dir).iterator
       if Completion.completed(s)(theory)
     } yield {
-      if (session == context_session || session_base.global_theories.isDefinedAt(theory)) theory
+      if (session == context_session || global_theory(theory)) theory
       else Long_Name.qualify(session, theory)
     }).toList.sorted
   }
diff -r 3d8b37b1d798 -r 8342cba8eae8 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Aug 17 14:42:20 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Wed Aug 17 15:18:17 2022 +0200
@@ -61,8 +61,6 @@
   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,
     proper_session_theories: List[Document.Node.Name] = Nil,
     document_theories: List[Document.Node.Name] = Nil,
     loaded_theories: Graph[String, Outer_Syntax] = Graph.string,  // cumulative imports
@@ -76,6 +74,8 @@
     session_graph_display: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil
   ) {
+    def session_entry: (String, Base) = session_name -> this
+
     override def toString: String =
       "Sessions.Base(session_name = " + quote(session_name) +
         ", loaded_theories = " + loaded_theories.size +
@@ -96,6 +96,8 @@
       nodes(name).syntax orElse loaded_theory_syntax(name) getOrElse overall_syntax
   }
 
+  val bootstrap_base: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
+
   sealed case class Deps(sessions_structure: Structure, session_bases: Map[String, Base]) {
     override def toString: String = "Sessions.Deps(" + sessions_structure + ")"
 
@@ -152,13 +154,9 @@
       }
     }
 
-    val bootstrap_bases = {
-      val base = sessions_structure.bootstrap
-      Map(base.session_name -> base)
-    }
-
     val session_bases =
-      sessions_structure.imports_topological_order.foldLeft(bootstrap_bases) {
+      sessions_structure.imports_topological_order.foldLeft(
+          Map(Sessions.bootstrap_base.session_entry)) {
         case (session_bases, session_name) =>
           progress.expose_interrupt()
 
@@ -333,8 +331,6 @@
               Base(
                 session_name = info.name,
                 session_pos = info.pos,
-                session_directories = sessions_structure.session_directories,
-                global_theories = sessions_structure.global_theories,
                 proper_session_theories = proper_session_theories,
                 document_theories = document_theories,
                 loaded_theories = dependencies.loaded_theories,
@@ -350,7 +346,7 @@
                   document_errors ::: dir_errors ::: sources_errors ::: path_errors :::
                   bibtex_errors)
 
-            session_bases + (info.name -> base)
+            session_bases + base.session_entry
           }
           catch {
             case ERROR(msg) =>
@@ -736,11 +732,7 @@
   ) {
     sessions_structure =>
 
-    def bootstrap: Base =
-      Base(
-        session_directories = session_directories,
-        global_theories = global_theories,
-        overall_syntax = Thy_Header.bootstrap_syntax)
+    def bootstrap: Base = Base(overall_syntax = Thy_Header.bootstrap_syntax)
 
     def dest_session_directories: List[(String, String)] =
       for ((file, session) <- session_directories.toList)