src/Pure/System/invoke_scala.scala
author wenzelm
Sun, 10 Jul 2011 23:46:05 +0200
changeset 43744 2c7e1565b4a3
child 43748 c70bd78ec83c
permissions -rw-r--r--
some support to invoke Scala methods under program control;
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
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
     4
Invoke static methods (String)String via reflection.
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
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    10
import java.lang.reflect.{Method, Modifier}
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    11
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
object Invoke_Scala
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    14
{
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    15
  private val STRING = Class.forName("java.lang.String")
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    16
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    17
  def method(class_name: String, method_name: String): String => String =
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    18
  {
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    19
    val m =
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    20
      try { Class.forName(class_name).getMethod(method_name, STRING) }
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    21
      catch {
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    22
        case _: ClassNotFoundException =>
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    23
          error("Class not found: " + quote(class_name))
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    24
        case _: NoSuchMethodException =>
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    25
          error("No such method: " + quote(class_name + "." + method_name))
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    26
      }
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    27
    if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString)
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    28
    if (m.getReturnType != STRING) error("Bad return type of method: " + m.toString)
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    29
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    30
    (s: String) => m.invoke(null, s).asInstanceOf[String]
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    31
  }
2c7e1565b4a3 some support to invoke Scala methods under program control;
wenzelm
parents:
diff changeset
    32
}