--- a/src/Doc/Implementation/ML.thy Thu Dec 11 23:42:03 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Dec 12 14:30:33 2014 +0100
@@ -2019,8 +2019,8 @@
individual exceptions by conventional @{verbatim "handle"} of ML.
\item @{ML Par_Exn.release_first} is similar to @{ML
- Par_Exn.release_all}, but only the first exception that has occurred
- in the original evaluation process is raised again, the others are
+ Par_Exn.release_all}, but only the first (meaningful) exception that has
+ occurred in the original evaluation process is raised again, the others are
ignored. That single exception may get handled by conventional
means in ML.
--- a/src/Pure/General/exn.scala Thu Dec 11 23:42:03 2014 +0100
+++ b/src/Pure/General/exn.scala Fri Dec 12 14:30:33 2014 +0100
@@ -27,13 +27,10 @@
}
def release_first[A](results: List[Result[A]]): List[A] =
- if (results.forall({ case Res(_) => true case _ => false }))
- results.map(release(_))
- else
- results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
- case Some(Exn(exn)) => throw exn
- case _ => results match { case Exn(exn) :: _ => throw exn case _ => ??? }
- }
+ results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
+ case Some(Exn(exn)) => throw exn
+ case _ => results.map(release(_))
+ }
/* interrupts */