src/Pure/System/invoke_scala.scala
changeset 44158 fe6d1ae7a065
parent 43751 8c7f69f1825b
child 49173 fa01a202399c
equal deleted inserted replaced
44157:a21d3e1e64fd 44158:fe6d1ae7a065
    55     Exn.capture { get_method(name) } match {
    55     Exn.capture { get_method(name) } match {
    56       case Exn.Res(f) =>
    56       case Exn.Res(f) =>
    57         Exn.capture { f(arg) } match {
    57         Exn.capture { f(arg) } match {
    58           case Exn.Res(null) => (Tag.NULL, "")
    58           case Exn.Res(null) => (Tag.NULL, "")
    59           case Exn.Res(res) => (Tag.OK, res)
    59           case Exn.Res(res) => (Tag.OK, res)
    60           case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
    60           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    61           case Exn.Exn(e) => (Tag.ERROR, e.toString)
       
    62         }
    61         }
    63       case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    62       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    64       case Exn.Exn(e) => (Tag.FAIL, e.toString)
       
    65     }
    63     }
    66 }
    64 }