more direct access to session_sources, without somewhat fragile file-system operations;
--- 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)))
}
--- 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)))
}
--- 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)