equal
deleted
inserted
replaced
117 |
117 |
118 |
118 |
119 /* message */ |
119 /* message */ |
120 |
120 |
121 def user_message(exn: Throwable): Option[String] = |
121 def user_message(exn: Throwable): Option[String] = |
122 if (exn.getClass == classOf[RuntimeException] || |
122 if (exn.isInstanceOf[User_Error] || exn.getClass == classOf[RuntimeException]) |
123 exn.getClass == classOf[User_Error]) |
|
124 { |
123 { |
125 Some(proper_string(exn.getMessage) getOrElse "Error") |
124 Some(proper_string(exn.getMessage) getOrElse "Error") |
126 } |
125 } |
127 else if (exn.isInstanceOf[java.sql.SQLException]) |
126 else if (exn.isInstanceOf[java.sql.SQLException]) |
128 { |
127 { |