src/Pure/System/invoke_scala.scala
author wenzelm
Mon Jul 11 16:48:02 2011 +0200 (2011-07-11)
changeset 43748 c70bd78ec83c
parent 43744 2c7e1565b4a3
child 43751 8c7f69f1825b
permissions -rw-r--r--
JVM method invocation service via Scala layer;
     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}
    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 =>
    28               error("Class not found: " + quote(class_name))
    29             case _: NoSuchMethodException =>
    30               error("No such method: " + quote(class_name + "." + method_name))
    31           }
    32         if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
    33         if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
    34 
    35         (arg: String) => m.invoke(null, arg).asInstanceOf[String]
    36       case _ => error("Malformed method name: " + quote(name))
    37     }
    38 
    39 
    40   /* method invocation */
    41 
    42   object Tag extends Enumeration
    43   {
    44     val NULL = Value("0")
    45     val OK = Value("1")
    46     val ERROR = Value("2")
    47     val FAIL = Value("3")
    48   }
    49 
    50   def method(name: String, arg: String): (Tag.Value, String) =
    51     Exn.capture { get_method(name) } match {
    52       case Exn.Res(f) =>
    53         Exn.capture { f(arg) } match {
    54           case Exn.Res(null) => (Tag.NULL, "")
    55           case Exn.Res(res) => (Tag.OK, res)
    56           case Exn.Exn(ERROR(msg)) => (Tag.ERROR, msg)
    57           case Exn.Exn(e) => throw e
    58         }
    59       case Exn.Exn(ERROR(msg)) => (Tag.FAIL, msg)
    60       case Exn.Exn(e) => throw e
    61     }
    62 }