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)))
     }