src/Pure/System/invoke_scala.scala
changeset 56667 65e84b0ef974
parent 56387 d92eb5c3960d
child 56730 e723f041b6d0
equal deleted inserted replaced
56666:229309cbc508 56667:65e84b0ef974
    56     Exn.capture { get_method(name) } match {
    56     Exn.capture { get_method(name) } match {
    57       case Exn.Res(f) =>
    57       case Exn.Res(f) =>
    58         Exn.capture { f(arg) } match {
    58         Exn.capture { f(arg) } match {
    59           case Exn.Res(null) => (Tag.NULL, "")
    59           case Exn.Res(null) => (Tag.NULL, "")
    60           case Exn.Res(res) => (Tag.OK, res)
    60           case Exn.Res(res) => (Tag.OK, res)
    61           case Exn.Exn(_: InterruptedException) => (Tag.INTERRUPT, "")
    61           case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "")
    62           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    62           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    63         }
    63         }
    64       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    64       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    65     }
    65     }
    66 }
    66 }