src/Pure/PIDE/command.scala

--- a/src/Pure/PIDE/command.scala	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Sep 19 19:48:54 2023 +0200
@@ -497,7 +497,7 @@
   def blobs: List[Exn.Result[Command.Blob]] = blobs_info.blobs
   def blobs_index: Int = blobs_info.index
 
-  def blobs_ok: Boolean = blobs.forall(Exn.the_res.isDefinedAt)
+  def blobs_ok: Boolean = blobs.forall(Exn.is_res)
 
   def blobs_names: List[Document.Node.Name] =
     for (case Exn.Res(blob) <- blobs) yield blob.name