# HG changeset patch
# User wenzelm
# Date 1672934422 -3600
# Node ID a8eb5046b05f7e1f71ccf71cf3e15033e0915d0a
# Parent  ca872f20cf5bc4173d88d3cf5ff8c6735763a9d5
tuned signature;

diff -r ca872f20cf5b -r a8eb5046b05f src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Jan 05 17:00:22 2023 +0100
@@ -26,6 +26,9 @@
   object Blobs_Info {
     val none: Blobs_Info = Blobs_Info(Nil)
 
+    def make(blobs: List[(Blob, Document.Blobs.Item)]): Blobs_Info =
+      if (blobs.isEmpty) none else Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
+
     def errors(msgs: List[String]): Blobs_Info =
       Blobs_Info(msgs.map(msg => Exn.Exn[Blob](ERROR(msg))))
   }
diff -r ca872f20cf5b -r a8eb5046b05f 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]) {
diff -r ca872f20cf5b -r a8eb5046b05f src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Jan 05 16:44:15 2023 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Jan 05 17:00:22 2023 +0100
@@ -71,10 +71,10 @@
       val command =
         Command.unparsed(thy_source, theory = true, id = id,
           node_name = Document.Node.Name(thy_file, theory = theory_context.theory),
-          blobs_info = Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a)),
+          blobs_info = Command.Blobs_Info.make(blobs),
           markups = markups, results = results)
 
-      val doc_blobs = Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
+      val doc_blobs = Document.Blobs.make(blobs)
 
       Document.State.init.snippet(command, doc_blobs)
     }
@@ -298,16 +298,10 @@
           override val cache: Term.Cache = store.cache
 
           override def build_blobs_info(node_name: Document.Node.Name): Command.Blobs_Info =
-            session_blobs(node_name) match {
-              case Nil => Command.Blobs_Info.none
-              case blobs => Command.Blobs_Info(for ((a, _) <- blobs) yield Exn.Res(a))
-            }
+            Command.Blobs_Info.make(session_blobs(node_name))
 
           override def build_blobs(node_name: Document.Node.Name): Document.Blobs =
-            session_blobs(node_name) match {
-              case Nil => Document.Blobs.empty
-              case blobs => Document.Blobs((for ((a, b) <- blobs.iterator) yield a.name -> b).toMap)
-            }
+            Document.Blobs.make(session_blobs(node_name))
         }
 
       object Build_Session_Errors {