clarified exceptions;
authorwenzelm
Sun, 04 Sep 2016 21:41:08 +0200
changeset 63782 aced4f0d1ad4
parent 63781 af9fe0b6b78e
child 63783 baa20f3b6cea
clarified exceptions;
src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Sun Sep 04 21:09:18 2016 +0200
+++ b/src/Pure/General/exn.scala	Sun Sep 04 21:41:08 2016 +0200
@@ -124,6 +124,11 @@
       val msg = exn.getMessage
       Some(if (msg == null || msg == "") "Error" else msg)
     }
+    else if (exn.isInstanceOf[java.sql.SQLException])
+    {
+      val msg = exn.getMessage
+      Some(if (msg == null || msg == "") "SQL error" else msg)
+    }
     else if (exn.isInstanceOf[java.io.IOException])
     {
       val msg = exn.getMessage