src/Pure/System/invoke_scala.scala
author wenzelm
Fri Aug 12 11:41:26 2011 +0200 (2011-08-12)
changeset 44158 fe6d1ae7a065
parent 43751 8c7f69f1825b
child 49173 fa01a202399c
permissions -rw-r--r--
clarified Exn.message;
     1 /*  Title:      Pure/System/invoke_scala.scala
     2     Author:     Makarius
     3 
     4 JVM method invocation service via Scala layer.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 import java.lang.reflect.{Method, Modifier, InvocationTargetException}
    11 import scala.util.matching.Regex
    12 
    13 
    14 object Invoke_Scala
    15 {
    16   /* method reflection */
    17 
    18   private val Ext = new Regex("(.*)\\.([^.]*)")
    19   private val STRING = Class.forName("java.lang.String")
    20 
    21   private def get_method(name: String): String => String =
    22     name match {
    23       case Ext(class_name, method_name) =>
    24         val m =
    25           try { Class.forName(class_name).getMethod(method_name, STRING) }
    26           catch {
    27             case _: ClassNotFoundException | _: NoSuchMethodException =>
    28               error("No such method: " + quote(name))
    29           }
    30         if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    31         if (m.getReturnType != STRING) error("Bad method return type: " + m.toString)
    32 
    33         (arg: String) => {
    34           try { m.invoke(null, arg).asInstanceOf[String] }
    35           catch {
    36             case e: InvocationTargetException if e.getCause != null =>
    37               throw e.getCause
    38           }
    39         }
    40       case _ => error("Malformed method name: " + quote(name))
    41     }
    42 
    43 
    44   /* method invocation */
    45 
    46   object Tag extends Enumeration
    47   {
    48     val NULL = Value("0")
    49     val OK = Value("1")
    50     val ERROR = Value("2")
    51     val FAIL = Value("3")
    52   }
    53 
    54   def method(name: String, arg: String): (Tag.Value, String) =
    55     Exn.capture { get_method(name) } match {
    56       case Exn.Res(f) =>
    57         Exn.capture { f(arg) } match {
    58           case Exn.Res(null) => (Tag.NULL, "")
    59           case Exn.Res(res) => (Tag.OK, res)
    60           case Exn.Exn(e) => (Tag.ERROR, Exn.message(e))
    61         }
    62       case Exn.Exn(e) => (Tag.FAIL, Exn.message(e))
    63     }
    64 }