basic support to reload theory markup from session store;

--- a/src/Pure/Build/build.scala	Sat Jun 28 17:12:41 2025 +0200
+++ b/src/Pure/Build/build.scala	Sun Jun 29 14:17:49 2025 +0200
@@ -707,7 +707,8 @@
 
   def read_theory(
     theory_context: Export.Theory_Context,
-    unicode_symbols: Boolean = false
+    unicode_symbols: Boolean = false,
+    migrate_file: String => String = identity
   ): Option[Document.Snapshot] = {
     def decode(str: String): String = Symbol.output(unicode_symbols, str)
 
@@ -721,19 +722,22 @@
 
     for {
       id <- theory_context.document_id()
-      (thy_file, blobs_files) <- theory_context.files(permissive = true)
+      (thy_file0, blobs_files0) <- theory_context.files(permissive = true)
     }
     yield {
+      val thy_file = migrate_file(thy_file0)
+
       val master_dir =
         Path.explode(Url.strip_base_name(thy_file).getOrElse(
           error("Cannot determine theory master directory: " + quote(thy_file))))
 
       val blobs =
-        blobs_files.map { name =>
+        blobs_files0.map { name0 =>
+          val name = migrate_file(name0)
           val path = Path.explode(name)
           val src_path = File.perhaps_relative_path(master_dir, path)
 
-          val file = read_source_file(name)
+          val file = read_source_file(name0)
           val bytes = file.bytes
           val text = decode(bytes.text)
           val chunk = Symbol.Text_Chunk(text)
@@ -742,7 +746,7 @@
             Document.Blobs.Item(bytes, text, chunk, changed = false)
         }
 
-      val thy_source = decode(read_source_file(thy_file).bytes.text)
+      val thy_source = decode(read_source_file(thy_file0).bytes.text)
       val thy_xml = read_xml(Export.MARKUP)
       val blobs_xml =
         for (i <- (1 to blobs.length).toList)

--- a/src/Pure/PIDE/session.scala	Sat Jun 28 17:12:41 2025 +0200
+++ b/src/Pure/PIDE/session.scala	Sun Jun 29 14:17:49 2025 +0200
@@ -12,6 +12,9 @@
 import scala.collection.mutable
 import scala.annotation.tailrec
 
+import java.util.{Collections, WeakHashMap, Map => JMap}
+import java.lang.ref.WeakReference
+
 
 object Session {
   /* outlets */
@@ -152,6 +155,28 @@
       store, resources.session_background, document_snapshot = document_snapshot)
   }
 
+  private val read_theory_cache = new WeakHashMap[String, WeakReference[Command]]
+
+  def read_theory(name: String): Command =
+    read_theory_cache.synchronized {
+      Option(read_theory_cache.get(name)).map(_.get) match {
+        case Some(command: Command) => command
+        case _ =>
+          val snapshot =
+            using(open_session_context()) { session_context =>
+              Build.read_theory(session_context.theory(name),
+                unicode_symbols = true,
+                migrate_file = (a: String) => session.resources.append_path("", Path.explode(a)))
+            }
+          snapshot.map(_.snippet_commands) match {
+            case Some(List(command)) =>
+              read_theory_cache.put(name, new WeakReference(command))
+              command
+            case _ => error("Failed to load theory " + quote(name) + " from session database")
+          }
+      }
+    }
+
 
   /* global flags */
 
@@ -452,7 +477,7 @@
             }
           }
 
-          if (!global_state.value.defined_command(command.id)) {
+          if (!command.span.is_theory && !global_state.value.defined_command(command.id)) {
             global_state.change(_.define_command(command))
             id_commands += command
           }

--- a/src/Pure/Thy/thy_syntax.scala	Sat Jun 28 17:12:41 2025 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Jun 29 14:17:49 2025 +0200
@@ -76,7 +76,7 @@
     val doc_edits = new mutable.ListBuffer[Document.Edit_Command]
 
     edits foreach {
-      case (name, Document.Node.Deps(header)) =>
+      case (name, Document.Node.Deps(header)) if !session_base.loaded_theory(name) =>
         val node = nodes(name)
         val update_header =
           node.header.errors.nonEmpty || header.errors.nonEmpty || node.header != header
@@ -149,6 +149,33 @@
   }
 
 
+  /* reload theory from session store */
+
+  def reload_theory(
+    session: Session,
+    doc_blobs: Document.Blobs,
+    theory_name: String,
+    theory_node: Document.Node,
+  ): Document.Node = {
+    val command = session.read_theory(theory_name)  // FIXME handle errors
+
+    val thy_ok = command.source == theory_node.source
+    val blobs_changed =
+      for {
+        case Exn.Res(blob) <- command.blobs
+        (digest, _) <- blob.content
+        doc_blob <- doc_blobs.get(blob.name)
+        if digest != doc_blob.bytes.sha1_digest
+      } yield blob.name
+
+    val command1 =
+      if (thy_ok && blobs_changed.isEmpty) command
+      else command // FIXME errors as markup
+
+    theory_node.update_commands(Linear_Set(command1))
+  }
+
+
   /* reparse range of command spans */
 
   @tailrec private def chop_common(
@@ -172,6 +199,8 @@
     first: Command,
     last: Command
   ): Linear_Set[Command] = {
+    require(!resources.session_base.loaded_theory(node_name))
+
     val cmds0 = commands.iterator(first, last).toList
     val blobs_spans0 =
       syntax.parse_spans(cmds0.iterator.map(_.source).mkString).map(span =>
@@ -219,6 +248,8 @@
     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(
@@ -250,13 +281,17 @@
       case (name, Document.Node.Edits(text_edits)) =>
         if (name.is_theory) {
           val commands1 = edit_text(text_edits, node.commands)
-          val commands2 = recover_spans(name, node.perspective.visible, commands1)
+          val commands2 =
+            if (session_base.loaded_theory(name)) commands1
+            else recover_spans(name, node.perspective.visible, commands1)
           node.update_commands(commands2)
         }
         else node
 
       case (_, Document.Node.Deps(_)) => node
 
+      case (name, Document.Node.Perspective(_, _, _)) if session_base.loaded_theory(name) => node
+
       case (name, Document.Node.Perspective(required, text_perspective, overlays)) =>
         val (visible, visible_overlay) = command_perspective(node, text_perspective, overlays)
         val perspective: Document.Node.Perspective_Command.T =
@@ -336,17 +371,20 @@
             val commands = node.commands
 
             val node1 =
-              if (reparse_set(name) && commands.nonEmpty) {
+              if (!session_base.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))
+                  commands, commands.head, commands.last))
               }
               else node
             val node2 =
               edits.foldLeft(node1)(
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit, _, _))
             val node3 =
-              if (reparse_set(name)) {
+              if (session_base.loaded_theory(name)) {
+                reload_theory(session, doc_blobs, name.theory, node)
+              }
+              else if (reparse_set(name)) {
                 text_edit(resources, syntax, get_blob, can_import, reparse_limit,
                   node2, (name, node2.edit_perspective))
               }
@@ -356,7 +394,9 @@
               doc_edits += (name -> node3.perspective)
             }
 
-            doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
+            if (!session_base.loaded_theory(name)) {
+              doc_edits += (name -> Document.Node.Edits(diff_commands(commands, node3.commands)))
+            }
 
             nodes += (name -> node3)
         }