src/Pure/General/exn.scala
changeset 48476 44f56fe01528
parent 45673 cd41e3903fbf
child 48479 819f7a5f3e7f
equal deleted inserted replaced
48475:02dd825f5a4e 48476:44f56fe01528
    30   /* message */
    30   /* message */
    31 
    31 
    32   private val runtime_exception = Class.forName("java.lang.RuntimeException")
    32   private val runtime_exception = Class.forName("java.lang.RuntimeException")
    33 
    33 
    34   def message(exn: Throwable): String =
    34   def message(exn: Throwable): String =
    35     if (exn.getClass == runtime_exception) {
    35     if (exn.isInstanceOf[java.io.IOException]) {
       
    36       val msg = exn.getMessage
       
    37       if (msg == null) "I/O error"
       
    38       else "I/O error: " + msg
       
    39     }
       
    40     else if (exn.getClass == runtime_exception) {
    36       val msg = exn.getMessage
    41       val msg = exn.getMessage
    37       if (msg == null) "Error" else msg
    42       if (msg == null) "Error" else msg
    38     }
    43     }
    39     else exn.toString
    44     else exn.toString
    40 }
    45 }