src/Pure/General/exn.scala
changeset 52066 83b7b88770c9
parent 51255 9db9e8c608ea
child 56667 65e84b0ef974
--- a/src/Pure/General/exn.scala	Sat May 18 12:41:31 2013 +0200
+++ b/src/Pure/General/exn.scala	Sat May 18 13:00:05 2013 +0200
@@ -47,23 +47,5 @@
     user_message(exn) getOrElse
       (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
        else 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
-        }
-    }
-  }
 }