clarified session sources: theory and blobs are read from database, instead of physical file-system;

--- a/src/Pure/PIDE/command.scala	Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Jan 05 16:44:15 2023 +0100
@@ -19,8 +19,6 @@
     src_path: Path,
     content: Option[(SHA1.Digest, Symbol.Text_Chunk)]
   ) {
-    def read_file: Bytes = Bytes.read(name.path)
-
     def chunk_file: Symbol.Text_Chunk.File =
       Symbol.Text_Chunk.File(name.node)
   }
@@ -111,6 +109,7 @@
   object Markup_Index {
     val markup: Markup_Index = Markup_Index(false, Symbol.Text_Chunk.Default)
     def blob(blob: Blob): Markup_Index = Markup_Index(false, blob.chunk_file)
+    def make(blobs: List[Blob]): List[Markup_Index] = markup :: blobs.map(blob)
   }
 
   sealed case class Markup_Index(status: Boolean, chunk_name: Symbol.Text_Chunk.Name)

--- a/src/Pure/PIDE/document.scala	Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 16:44:15 2023 +0100
@@ -603,7 +603,7 @@
 
     /* command as add-on snippet */
 
-    def snippet(command: Command): Snapshot = {
+    def snippet(command: Command, doc_blobs: Blobs): Snapshot = {
       val node_name = command.node_name
 
       val nodes0 = version.nodes
@@ -611,7 +611,9 @@
       val version1 = Version.make(nodes1)
 
       val edits: List[Edit_Text] =
-        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source))))
+        List(node_name -> Node.Edits(List(Text.Edit.insert(0, command.source)))) :::
+        (for (blob_name <- command.blobs_names; blob <- doc_blobs.get(blob_name))
+          yield blob_name -> Node.Blob(blob))
 
       val state0 = state.define_command(command)
       val state1 =
@@ -638,15 +640,9 @@
         case Some(command) =>
           for (Exn.Res(blob) <- command.blobs)
           yield {
-            val bytes = blob.read_file
-            val text = bytes.text
-            val xml =
-              if (Bytes(text) == bytes) {
-                val markup = command.init_markups(Command.Markup_Index.blob(blob))
-                markup.to_XML(Text.Range.length(text), text, elements)
-              }
-              else Nil
-            blob -> xml
+            val text = get_node(blob.name).source
+            val markup = command.init_markups(Command.Markup_Index.blob(blob))
+            blob -> markup.to_XML(Text.Range.length(text), text, elements)
           }
       }
     }
@@ -1003,17 +999,18 @@
       }
     }
 
-    def end_theory(id: Document_ID.Exec): (Snapshot, State) =
+    def end_theory(id: Document_ID.Exec, document_blobs: Node.Name => Blobs): (Snapshot, State) =
       theories.get(id) match {
         case None => fail
         case Some(st) =>
           val command = st.command
           val node_name = command.node_name
+          val doc_blobs = document_blobs(node_name)
           val command1 =
             Command.unparsed(command.source, theory = true, id = id, node_name = node_name,
               blobs_info = command.blobs_info, results = st.results, markups = st.markups)
           val state1 = copy(theories = theories - id)
-          (state1.snippet(command1), state1)
+          (state1.snippet(command1, doc_blobs), state1)
       }
 
     def assign(
@@ -1250,7 +1247,7 @@
       new Snapshot(this, version, node_name, pending_edits1, snippet_command)
     }
 
-    def snippet(command: Command): Snapshot =
-      snapshot().snippet(command)
+    def snippet(command: Command, doc_blobs: Blobs): Snapshot =
+      snapshot().snippet(command, doc_blobs)
   }
 }

--- a/src/Pure/PIDE/session.scala	Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Pure/PIDE/session.scala	Thu Jan 05 16:44:15 2023 +0100
@@ -125,8 +125,8 @@
 
   val cache: Term.Cache = Term.Cache.make()
 
-  def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info =
-    Command.Blobs_Info.none
+  def build_blobs_info(name: Document.Node.Name): Command.Blobs_Info = Command.Blobs_Info.none
+  def build_blobs(name: Document.Node.Name): Document.Blobs = Document.Blobs.empty
 
 
   /* global flags */
@@ -560,7 +560,7 @@
             case Markup.Process_Result(result) if output.is_exit =>
               if (prover.defined) protocol_handlers.exit()
               for (id <- global_state.value.theories.keys) {
-                val snapshot = global_state.change_result(_.end_theory(id))
+                val snapshot = global_state.change_result(_.end_theory(id, build_blobs))
                 finished_theories.post(snapshot)
               }
               file_formats.stop_session()

--- a/src/Pure/Tools/build_job.scala	Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Jan 05 16:44:15 2023 +0100
@@ -25,6 +25,9 @@
         Symbol.output(unicode_symbols, UTF8.decode_permissive(read(name).bytes)),
         cache = theory_context.cache)
 
+    def read_source_file(name: String): Sessions.Source_File =
+      theory_context.session_context.source_file(name)
+
     for {
       id <- theory_context.document_id()
       (thy_file, blobs_files) <- theory_context.files(permissive = true)
@@ -35,31 +38,26 @@
           error("Cannot determine theory master directory: " + quote(thy_file))))
 
       val blobs =
-        blobs_files.map { file =>
-          val name = Document.Node.Name(file)
-          val path = Path.explode(file)
+        blobs_files.map { name =>
+          val path = Path.explode(name)
           val src_path = File.relative_path(master_dir, path).getOrElse(path)
-          Command.Blob(name, src_path, None)
+
+          val file = read_source_file(name)
+          val bytes = file.bytes
+          val text = bytes.text
+          val chunk = Symbol.Text_Chunk(text)
+
+          Command.Blob(Document.Node.Name(name), src_path, Some((file.digest, chunk))) ->
+            Document.Blobs.Item(bytes, text, chunk, changed = false)
         }
+
+      val thy_source = read_source_file(thy_file).text
+      val thy_xml = read_xml(Export.MARKUP)
       val blobs_xml =
         for (i <- (1 to blobs.length).toList)
           yield read_xml(Export.MARKUP + i)
 
-      val blobs_info =
-        Command.Blobs_Info(
-          for { (Command.Blob(name, src_path, _), xml) <- blobs zip blobs_xml }
-            yield {
-              val text = XML.content(xml)
-              val chunk = Symbol.Text_Chunk(text)
-              val digest = SHA1.digest(Symbol.encode(text))
-              Exn.Res(Command.Blob(name, src_path, Some((digest, chunk))))
-            })
-
-      val thy_xml = read_xml(Export.MARKUP)
-      val thy_source = XML.content(thy_xml)
-
-      val markups_index =
-        Command.Markup_Index.markup :: blobs.map(Command.Markup_Index.blob)
+      val markups_index = Command.Markup_Index.make(blobs.map(_._1))
       val markups =
         Command.Markups.make(
           for ((index, xml) <- markups_index.zip(thy_xml :: blobs_xml))
@@ -73,9 +71,12 @@
       val command =
         Command.unparsed(thy_source, theory = true, id = id,
           node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
-          blobs_info = blobs_info, markups = markups, results = results)
+          blobs_info = Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)),
+          markups = markups, results = results)
 
-      Document.State.init.snippet(command)
+      val doc_blobs = Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
+
+      Document.State.init.snippet(command, doc_blobs)
     }
   }
 
@@ -269,32 +270,44 @@
         }
         else Nil
 
+      def session_blobs(node_name: Document.Node.Name): List[(Command.Blob, Document.Blobs.Item)] =
+        session_background.base.theory_load_commands.get(node_name.theory) match {
+          case None => Nil
+          case Some(spans) =>
+            val syntax = session_background.base.theory_syntax(node_name)
+            val master_dir = Path.explode(node_name.master_dir)
+            for (span <- spans; file <- span.loaded_files(syntax).files)
+              yield {
+                val src_path = Path.explode(file)
+                val blob_name = Document.Node.Name(File.symbolic_path(master_dir + src_path))
+
+                val bytes = session_sources(blob_name.node).bytes
+                val text = bytes.text
+                val chunk = Symbol.Text_Chunk(text)
+
+                Command.Blob(blob_name, src_path, Some((SHA1.digest(bytes), chunk))) ->
+                  Document.Blobs.Item(bytes, text, chunk, changed = false)
+              }
+        }
+
       val resources =
         new Resources(session_background, log = log, command_timings = command_timings0)
+
       val session =
         new Session(options, resources) {
           override val cache: Term.Cache = store.cache
 
-          override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info = {
-            session_background.base.theory_load_commands.get(node_name.theory) match {
-              case Some(spans) =>
-                val syntax = session_background.base.theory_syntax(node_name)
-                val blobs =
-                  for (span <- spans; file <- span.loaded_files(syntax).files)
-                  yield {
-                    (Exn.capture {
-                      val master_dir = Path.explode(node_name.master_dir)
-                      val src_path = Path.explode(file)
-                      val node = File.symbolic_path(master_dir + src_path)
-                      val bytes = session_sources(node).bytes
-                      val content = (SHA1.digest(bytes), Symbol.Text_Chunk(bytes.text))
-                      Command.Blob(Document.Node.Name(node), src_path, Some(content))
-                    }).user_error
-                  }
-                Command.Blobs_Info(blobs)
-              case None => Command.Blobs_Info.none
+          override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
+            session_blobs(node_name) match {
+              case Nil => Command.Blobs_Info.none
+              case blobs => Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
             }
-          }
+
+          override def build_blobs(node_name: Document.Node.Name): Document.Blobs =
+            session_blobs(node_name) match {
+              case Nil => Document.Blobs.empty
+              case blobs => Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
+            }
         }
 
       object Build_Session_Errors {

--- a/src/Tools/jEdit/src/jedit_rendering.scala	Thu Jan 05 12:43:05 2023 +0100
+++ b/src/Tools/jEdit/src/jedit_rendering.scala	Thu Jan 05 16:44:15 2023 +0100
@@ -31,7 +31,7 @@
     results: Command.Results = Command.Results.empty
   ): (String, JEdit_Rendering) = {
     val command = Command.rich_text(Document_ID.make(), results, formatted_body)
-    val snippet = snapshot.snippet(command)
+    val snippet = snapshot.snippet(command, Document.Blobs.empty)
     val model = File_Model.init(PIDE.session)
     val rendering = apply(snippet, model, PIDE.options.value)
     (command.source, rendering)