--- a/src/Pure/General/exn.scala Fri Dec 07 16:25:33 2012 +0100
+++ b/src/Pure/General/exn.scala Fri Dec 07 16:33:17 2012 +0100
@@ -45,5 +45,23 @@
def message(exn: Throwable): String =
user_message(exn) getOrElse exn.toString
+
+
+ /* recover from spurious crash */
+
+ def recover[A](e: => A): A =
+ {
+ capture(e) match {
+ case Res(x) => x
+ case Exn(exn) =>
+ capture(e) match {
+ case Res(x) =>
+ java.lang.System.err.println("Recovered from spurious crash after retry!")
+ exn.printStackTrace()
+ x
+ case Exn(_) => throw exn
+ }
+ }
+ }
}