# HG changeset patch
# User wenzelm
# Date 1361635968 -3600
# Node ID 9db9e8c608ea890cfdffe3dc6f44abe8788e5ffa
# Parent  5bae6fc0e125dcdbd212ab3274adc155b8ff41ff
more friendly message for spurious InterruptedException, which might still occur due to JVM oddities;

diff -r 5bae6fc0e125 -r 9db9e8c608ea src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Sat Feb 23 15:08:53 2013 +0100
+++ b/src/Pure/General/exn.scala	Sat Feb 23 17:12:48 2013 +0100
@@ -44,7 +44,9 @@
     else None
 
   def message(exn: Throwable): String =
-    user_message(exn) getOrElse exn.toString
+    user_message(exn) getOrElse
+      (if (exn.isInstanceOf[InterruptedException]) "Interrupt"
+       else exn.toString)
 
 
   /* recover from spurious crash */