# HG changeset patch # User wenzelm # Date 1689952013 -7200 # Node ID 48cbee2a6f2ed6d8345bf1712e25bec7c653dda2 # Parent 5b7d1cb073dbc2f3ff4589aec0b322b9c9c07057 clarified signature: more operations; diff -r 5b7d1cb073db -r 48cbee2a6f2e src/Pure/General/exn.scala --- 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) } diff -r 5b7d1cb073db -r 48cbee2a6f2e src/Pure/PIDE/command.scala --- 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 diff -r 5b7d1cb073db -r 48cbee2a6f2e src/Pure/Tools/build_job.scala --- 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)) {