clarified signature: more operations;

--- a/src/Pure/General/exn.scala	Fri Jul 21 14:14:48 2023 +0200
+++ b/src/Pure/General/exn.scala	Fri Jul 21 17:06:53 2023 +0200
@@ -53,6 +53,9 @@
   case class Res[A](res: A) extends Result[A]
   case class Exn[A](exn: Throwable) extends Result[A]
 
+  def the_res[A]: PartialFunction[Result[A], A] = { case Res(res) => res }
+  def the_exn[A]: PartialFunction[Result[A], Throwable] = { case Exn(exn) => exn }
+
   def capture[A](e: => A): Result[A] =
     try { Res(e) }
     catch { case exn: Throwable => Exn[A](exn) }

--- a/src/Pure/PIDE/command.scala	Fri Jul 21 14:14:48 2023 +0200
+++ b/src/Pure/PIDE/command.scala	Fri Jul 21 17:06:53 2023 +0200
@@ -497,8 +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({ case Exn.Res(_) => true case _ => false })
+  def blobs_ok: Boolean = blobs.forall(Exn.the_res.isDefinedAt)
 
   def blobs_names: List[Document.Node.Name] =
     for (Exn.Res(blob) <- blobs) yield blob.name

--- a/src/Pure/Tools/build_job.scala	Fri Jul 21 14:14:48 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Jul 21 17:06:53 2023 +0200
@@ -388,7 +388,7 @@
 
           val (document_output, document_errors) =
             try {
-              if (build_errors.isInstanceOf[Exn.Res[_]] && result0.ok && info.documents.nonEmpty) {
+              if (Exn.the_res.isDefinedAt(build_errors) && result0.ok && info.documents.nonEmpty) {
                 using(Export.open_database_context(store, server = server)) { database_context =>
                   val documents =
                     using(database_context.open_session(session_background)) {