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