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