# HG changeset patch
# User wenzelm
# Date 1695145734 -7200
# Node ID 88f47c70187a3e46f1b0a159b99c77b899773fc0
# Parent  90b12b919b5f7dbc9125a67d2ef7d066a85a5b62
clarified signature;

diff -r 90b12b919b5f -r 88f47c70187a src/Pure/Concurrent/par_exn.ML
--- a/src/Pure/Concurrent/par_exn.ML	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/Concurrent/par_exn.ML	Tue Sep 19 19:48:54 2023 +0200
@@ -58,11 +58,11 @@
 (* parallel results *)
 
 fun is_interrupted results =
-  exists (fn Exn.Exn _ => true | _ => false) results andalso
+  exists Exn.is_exn results andalso
     Exn.is_interrupt (make (map_filter Exn.get_exn results));
 
 fun release_all results =
-  if forall (fn Exn.Res _ => true | _ => false) results
+  if forall Exn.is_res results
   then map Exn.release results
   else raise make (map_filter Exn.get_exn results);
 
diff -r 90b12b919b5f -r 88f47c70187a src/Pure/General/exn.ML
--- a/src/Pure/General/exn.ML	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/General/exn.ML	Tue Sep 19 19:48:54 2023 +0200
@@ -17,6 +17,8 @@
   val polyml_location: exn -> PolyML.location option
   val reraise: exn -> 'a
   datatype 'a result = Res of 'a | Exn of exn
+  val is_res: 'a result -> bool
+  val is_exn: 'a result -> bool
   val get_res: 'a result -> 'a option
   val get_exn: 'a result -> exn option
   val capture: ('a -> 'b) -> 'a -> 'b result
@@ -62,6 +64,12 @@
   Res of 'a |
   Exn of exn;
 
+fun is_res (Res _) = true
+  | is_res _ = false;
+
+fun is_exn (Exn _) = true
+  | is_exn _ = false;
+
 fun get_res (Res x) = SOME x
   | get_res _ = NONE;
 
diff -r 90b12b919b5f -r 88f47c70187a src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/General/exn.scala	Tue Sep 19 19:48:54 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 is_res[A](result: Result[A]): Boolean = result.isInstanceOf[Res[A]]
+  def is_exn[A](result: Result[A]): Boolean = result.isInstanceOf[Exn[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 }
 
diff -r 90b12b919b5f -r 88f47c70187a 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
diff -r 90b12b919b5f -r 88f47c70187a src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Sep 19 19:48:54 2023 +0200
@@ -258,7 +258,7 @@
         capture(host, "open") { host.open_session(build_context, progress = progress) },
         remote_hosts, thread = true)
 
-    if (attempts.forall(Exn.the_res.isDefinedAt)) {
+    if (attempts.forall(Exn.is_res)) {
       _sessions = attempts.map(Exn.the_res)
       _sessions
     }
diff -r 90b12b919b5f -r 88f47c70187a src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Tue Sep 19 13:46:11 2023 +0200
+++ b/src/Pure/Tools/build_job.scala	Tue Sep 19 19:48:54 2023 +0200
@@ -391,7 +391,7 @@
 
           val (document_output, document_errors) =
             try {
-              if (Exn.the_res.isDefinedAt(build_errors) && result0.ok && info.documents.nonEmpty) {
+              if (Exn.is_res(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)) {