src/Pure/General/exn.scala

--- a/src/Pure/General/exn.scala	Thu May 04 12:30:19 2017 +0200
+++ b/src/Pure/General/exn.scala	Thu May 04 14:57:31 2017 +0200
@@ -120,13 +120,11 @@
     if (exn.getClass == classOf[RuntimeException] ||
         exn.getClass == classOf[User_Error])
     {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "Error" else msg)
+      Some(proper_string(exn.getMessage) getOrElse "Error")
     }
     else if (exn.isInstanceOf[java.sql.SQLException])
     {
-      val msg = exn.getMessage
-      Some(if (msg == null || msg == "") "SQL error" else msg)
+      Some(proper_string(exn.getMessage) getOrElse "SQL error")
     }
     else if (exn.isInstanceOf[java.io.IOException])
     {