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