# HG changeset patch
# User wenzelm
# Date 1672844016 -3600
# Node ID 4ef86dfe2296f8c0dcfe09231ce27c9e0b94e40f
# Parent  c84d2b259125fd750fffcb5af494e610e882ea33
tuned;

diff -r c84d2b259125 -r 4ef86dfe2296 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Jan 04 15:42:00 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Wed Jan 04 15:53:36 2023 +0100
@@ -14,13 +14,6 @@
 object Command {
   /* blobs */
 
-  object Blob {
-    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)))
-    }
-  }
-
   sealed case class Blob(
     name: Document.Node.Name,
     src_path: Path,
diff -r c84d2b259125 -r 4ef86dfe2296 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Wed Jan 04 15:42:00 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Wed Jan 04 15:53:36 2023 +0100
@@ -287,7 +287,8 @@
                       val src_path = Path.explode(file)
                       val node = File.symbolic_path(master_dir + src_path)
                       val bytes = session_sources(node).bytes
-                      Command.Blob.make(Document.Node.Name(node), src_path, 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)