src/Pure/General/exn.scala
changeset 65716 678e00851cfb
parent 65275 50f956a1ac3f
child 65828 02dd430d80c5
equal deleted inserted replaced
65715:e57e5935c6b4 65716:678e00851cfb
   118 
   118 
   119   def user_message(exn: Throwable): Option[String] =
   119   def user_message(exn: Throwable): Option[String] =
   120     if (exn.getClass == classOf[RuntimeException] ||
   120     if (exn.getClass == classOf[RuntimeException] ||
   121         exn.getClass == classOf[User_Error])
   121         exn.getClass == classOf[User_Error])
   122     {
   122     {
   123       val msg = exn.getMessage
   123       Some(proper_string(exn.getMessage) getOrElse "Error")
   124       Some(if (msg == null || msg == "") "Error" else msg)
       
   125     }
   124     }
   126     else if (exn.isInstanceOf[java.sql.SQLException])
   125     else if (exn.isInstanceOf[java.sql.SQLException])
   127     {
   126     {
   128       val msg = exn.getMessage
   127       Some(proper_string(exn.getMessage) getOrElse "SQL error")
   129       Some(if (msg == null || msg == "") "SQL error" else msg)
       
   130     }
   128     }
   131     else if (exn.isInstanceOf[java.io.IOException])
   129     else if (exn.isInstanceOf[java.io.IOException])
   132     {
   130     {
   133       val msg = exn.getMessage
   131       val msg = exn.getMessage
   134       Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)
   132       Some(if (msg == null || msg == "") "I/O error" else "I/O error: " + msg)