# HG changeset patch
# User wenzelm
# Date 1753711872 -7200
# Node ID 7bacb59eb631365b3f2d5adb993ef1eadba51ff6
# Parent  af85ea5d9b20b6f50a89824a31726bcda9844c6a
tuned signature;

diff -r af85ea5d9b20 -r 7bacb59eb631 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Mon Jul 28 16:10:02 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Mon Jul 28 16:11:12 2025 +0200
@@ -67,7 +67,7 @@
   /** header edits: graph structure and outer syntax **/
 
   private def header_edits(
-    session_base: Sessions.Base,
+    resources: Resources,
     previous: Document.Version,
     edits: List[Document.Edit_Text]
   ): (List[Document.Node.Name], Document.Nodes, List[Document.Edit_Command]) = {
@@ -76,7 +76,7 @@
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
 
     edits foreach {
-      case (name, Document.Node.Deps(header)) if !session_base.loaded_theory(name) =>
+      case (name, Document.Node.Deps(header)) if !resources.loaded_theory(name) =>
         val node = nodes(name)
         val update_header =
           node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
@@ -102,9 +102,9 @@
           val header = node.header
           val imports_syntax =
             if (header.imports.nonEmpty) {
-              Outer_Syntax.merge(header.imports.map(session_base.node_syntax(nodes, _)))
+              Outer_Syntax.merge(header.imports.map(resources.session_base.node_syntax(nodes, _)))
             }
-            else session_base.overall_syntax
+            else resources.session_base.overall_syntax
           Some(imports_syntax + header)
         }
       nodes += (name -> node.update_syntax(syntax))
@@ -219,7 +219,7 @@
     first: Command,
     last: Command
   ): Linear_Set[Command] = {
-    require(!resources.session_base.loaded_theory(node_name))
+    require(!resources.loaded_theory(node_name))
 
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
@@ -268,8 +268,6 @@
     node: Document.Node,
     edit: Document.Edit_Text
   ): Document.Node = {
-    val session_base = resources.session_base
-
     /* recover command spans after edits */
     // FIXME somewhat slow
     def recover_spans(
@@ -302,7 +300,7 @@
         if (name.is_theory) {
           val commands1 = edit_text(text_edits, node.commands)
           val commands2 =
-            if (session_base.loaded_theory(name)) commands1
+            if (resources.loaded_theory(name)) commands1
             else recover_spans(name, node.perspective.visible, commands1)
           node.update_commands(commands2)
         }
@@ -310,7 +308,7 @@
 
       case (_, Document.Node.Deps(_)) => node
 
-      case (name, Document.Node.Perspective(_, _, _)) if session_base.loaded_theory(name) => node
+      case (name, Document.Node.Perspective(_, _, _)) if resources.loaded_theory(name) => node
 
       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
@@ -355,16 +353,15 @@
     consolidate: List[Document.Node.Name]
   ): Session.Change = {
     val resources = session.resources
-    val session_base = resources.session_base
     val reparse_limit = session.reparse_limit
 
-    val (syntax_changed, nodes0, doc_edits0) = header_edits(session_base, previous, edits)
+    val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
 
     def get_blob(name: Document.Node.Name): Option[Document.Blobs.Item] =
       doc_blobs.get(name) orElse previous.nodes(name).get_blob
 
     def can_import(name: Document.Node.Name): Boolean =
-      session_base.loaded_theory(name) || nodes0(name).has_header
+      resources.loaded_theory(name) || nodes0(name).has_header
 
     val (doc_edits, version) =
       if (edits.isEmpty) (Nil, Document.Version.make(previous.nodes))
@@ -387,11 +384,11 @@
         node_edits foreach {
           case (name, edits) =>
             val node = nodes(name)
-            val syntax = session_base.node_syntax(nodes, name)
+            val syntax = resources.session_base.node_syntax(nodes, name)
             val commands = node.commands
 
             val node1 =
-              if (!session_base.loaded_theory(name) && reparse_set(name) && commands.nonEmpty) {
+              if (!resources.loaded_theory(name) && reparse_set(name) && commands.nonEmpty) {
                 node.update_commands(
                   reparse_spans(resources, syntax, get_blob, can_import, name,
                   commands, commands.head, commands.last))
@@ -401,7 +398,7 @@
               edits.foldLeft(node1)(
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
-              if (session_base.loaded_theory(name)) {
+              if (resources.loaded_theory(name)) {
                 reload_theory(session, doc_blobs, name, node2)
               }
               else if (reparse_set(name)) {
@@ -414,7 +411,7 @@
               doc_edits += (name -> node3.perspective)
             }
 
-            if (!session_base.loaded_theory(name)) {
+            if (!resources.loaded_theory(name)) {
               doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
             }