src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/PIDE/document.scala	Thu Jan 05 17:00:22 2023 +0100
@@ -48,6 +48,10 @@
 
     def apply(blobs: Map[Node.Name, Item]): Blobs = new Blobs(blobs)
     val empty: Blobs = apply(Map.empty)
+
+    def make(blobs: List[(Command.Blob, Item)]): Blobs =
+      if (blobs.isEmpty) empty
+      else apply((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
   }
 
   final class Blobs private(blobs: Map[Node.Name, Blobs.Item]) {