# HG changeset patch
# User wenzelm
# Date 1672843320 -3600
# Node ID c84d2b259125fd750fffcb5af494e610e882ea33
# Parent  2ccc5d380d88755651d7554609bc8bf860b6157f
more direct access to session_sources, without somewhat fragile file-system operations;

diff -r 2ccc5d380d88 -r c84d2b259125 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Jan 04 15:02:48 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Jan 04 15:42:00 2023 +0100
@@ -15,8 +15,7 @@
   /* blobs */
 
   object Blob {
-    def read_file(name: Document.Node.Name, src_path: Path): Blob = {
-      val bytes = Bytes.read(name.path)
+    def make(name: Document.Node.Name, src_path: Path, bytes: Bytes): Blob = {
       val chunk = Symbol.Text_Chunk(bytes.text)
       Blob(name, src_path, Some((bytes.sha1_digest, chunk)))
     }
diff -r 2ccc5d380d88 -r c84d2b259125 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Wed Jan 04 15:02:48 2023 +0100
+++ b/src/Pure/Thy/sessions.scala	Wed Jan 04 15:42:00 2023 +0100
@@ -109,6 +109,10 @@
   class Sources private(rep: Map[String, Source_File]) extends Iterable[Source_File] {
     override def toString: String = rep.values.toList.sortBy(_.name).mkString("Sources(", ", ", ")")
     override def iterator: Iterator[Source_File] = rep.valuesIterator
+
+    def get(name: String): Option[Source_File] = rep.get(name)
+    def apply(name: String): Source_File =
+      get(name).getOrElse(error("Missing session sources entry " + quote(name)))
   }
 
 
diff -r 2ccc5d380d88 -r c84d2b259125 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Jan 04 15:02:48 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Jan 04 15:42:00 2023 +0100
@@ -286,7 +286,8 @@
                       val master_dir = Path.explode(node_name.master_dir)
                       val src_path = Path.explode(file)
                       val node = File.symbolic_path(master_dir + src_path)
-                      Command.Blob.read_file(Document.Node.Name(node), src_path)
+                      val bytes = session_sources(node).bytes
+                      Command.Blob.make(Document.Node.Name(node), src_path, bytes)
                     }).user_error
                   }
                 Command.Blobs_Info(blobs)