# HG changeset patch
# User wenzelm
# Date 1354894397 -3600
# Node ID 027d405951c891543d0cc0ea733ab33dc33d2439
# Parent  ee729dbd1b7f5734aac22711bd07a4defae73e57
some support to recover from spurious crash -- this is Physics, not Mathematics;

diff -r ee729dbd1b7f -r 027d405951c8 src/Pure/General/exn.scala
--- 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
+        }
+    }
+  }
 }