author | wenzelm |
Thu, 19 Jul 2012 12:37:08 +0200 | |
changeset 48347 | 8bb27ab9e841 |
parent 44158 | fe6d1ae7a065 |
child 49173 | fa01a202399c |
permissions | -rw-r--r-- |
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 | 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 | 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 | 16 |
/* method reflection */ |
17 |
||
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 | 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 { |
|
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 | 29 |
} |
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 | 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 | 40 |
case _ => error("Malformed method name: " + quote(name)) |
41 |
} |
|
42 |
||
43 |
||
44 |
/* method invocation */ |
|
45 |
||
46 |
object Tag extends Enumeration |
|
43744
2c7e1565b4a3
some support to invoke Scala methods under program control;
wenzelm
parents:
diff
changeset
|
47 |
{ |
43748 | 48 |
val NULL = Value("0") |
49 |
val OK = Value("1") |
|
50 |
val ERROR = Value("2") |
|
51 |
val FAIL = Value("3") |
|
52 |
} |
|
43744
2c7e1565b4a3
some support to invoke Scala methods under program control;
wenzelm
parents:
diff
changeset
|
53 |
|
43748 | 54 |
def method(name: String, arg: String): (Tag.Value, String) = |
55 |
Exn.capture { get_method(name) } match { |
|
56 |
case Exn.Res(f) => |
|
57 |
Exn.capture { f(arg) } match { |
|
58 |
case Exn.Res(null) => (Tag.NULL, "") |
|
59 |
case Exn.Res(res) => (Tag.OK, res) |
|
44158 | 60 |
case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) |
43748 | 61 |
} |
44158 | 62 |
case Exn.Exn(e) => (Tag.FAIL, Exn.message(e)) |
43748 | 63 |
} |
43744
2c7e1565b4a3
some support to invoke Scala methods under program control;
wenzelm
parents:
diff
changeset
|
64 |
} |