proper InvocationTargetException.getCause for indirect exceptions;
authorwenzelm
Mon Jul 11 17:14:30 2011 +0200 (2011-07-11)
changeset 437518c7f69f1825b
parent 43750 390dbda4f3d7
child 43752 0517a69de5d6
proper InvocationTargetException.getCause for indirect exceptions;
capture hard errors to ensure protocol integrity;
tuned error messages;
src/Pure/System/invoke_scala.scala
     1.1 --- a/src/Pure/System/invoke_scala.scala	Mon Jul 11 17:11:54 2011 +0200
     1.2 +++ b/src/Pure/System/invoke_scala.scala	Mon Jul 11 17:14:30 2011 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  package isabelle
     1.5  
     1.6  
     1.7 -import java.lang.reflect.{Method, Modifier}
     1.8 +import java.lang.reflect.{Method, Modifier, InvocationTargetException}
     1.9  import scala.util.matching.Regex
    1.10  
    1.11  
    1.12 @@ -24,15 +24,19 @@
    1.13          val m =
    1.14            try { Class.forName(class_name).getMethod(method_name, STRING) }
    1.15            catch {
    1.16 -            case _: ClassNotFoundException =>
    1.17 -              error("Class not found: " + quote(class_name))
    1.18 -            case _: NoSuchMethodException =>
    1.19 -              error("No such method: " + quote(class_name + "." + method_name))
    1.20 +            case _: ClassNotFoundException | _: NoSuchMethodException =>
    1.21 +              error("No such method: " + quote(name))
    1.22            }
    1.23          if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    1.24 -        if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
    1.25 +        if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
    1.26  
    1.27 -        (arg: String) => m.invoke(null, arg).asInstanceOf[String]
    1.28 +        (arg: String) => {
    1.29 +          try { m.invoke(null, arg).asInstanceOf[String] }
    1.30 +          catch {
    1.31 +            case e: InvocationTargetException if e.getCause != null =>
    1.32 +              throw e.getCause
    1.33 +          }
    1.34 +        }
    1.35        case _ => error("Malformed method name: " + quote(name))
    1.36      }
    1.37  
    1.38 @@ -54,9 +58,9 @@
    1.39            case Exn.Res(null) => (Tag.NULL, "")
    1.40            case Exn.Res(res) => (Tag.OK, res)
    1.41            case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
    1.42 -          case Exn.Exn(e) => throw e
    1.43 +          case Exn.Exn(e) => (Tag.ERROR, e.toString)
    1.44          }
    1.45        case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    1.46 -      case Exn.Exn(e) => throw e
    1.47 +      case Exn.Exn(e) => (Tag.FAIL, e.toString)
    1.48      }
    1.49  }