|
1 /* Title: Pure/System/scala.scala |
|
2 Author: Makarius |
|
3 |
|
4 Support for Scala at runtime. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 import java.lang.reflect.{Method, Modifier, InvocationTargetException} |
|
11 |
|
12 import scala.util.matching.Regex |
|
13 |
|
14 |
|
15 object Scala |
|
16 { |
|
17 /** invoke JVM method via Isabelle/Scala **/ |
|
18 |
|
19 /* method reflection */ |
|
20 |
|
21 private val Ext = new Regex("(.*)\\.([^.]*)") |
|
22 private val STRING = Class.forName("java.lang.String") |
|
23 |
|
24 private def get_method(name: String): String => String = |
|
25 name match { |
|
26 case Ext(class_name, method_name) => |
|
27 val m = |
|
28 try { Class.forName(class_name).getMethod(method_name, STRING) } |
|
29 catch { |
|
30 case _: ClassNotFoundException | _: NoSuchMethodException => |
|
31 error("No such method: " + quote(name)) |
|
32 } |
|
33 if (!Modifier.isStatic(m.getModifiers)) error("Not at static method: " + m.toString) |
|
34 if (m.getReturnType != STRING) error("Bad method return type: " + m.toString) |
|
35 |
|
36 (arg: String) => { |
|
37 try { m.invoke(null, arg).asInstanceOf[String] } |
|
38 catch { |
|
39 case e: InvocationTargetException if e.getCause != null => |
|
40 throw e.getCause |
|
41 } |
|
42 } |
|
43 case _ => error("Malformed method name: " + quote(name)) |
|
44 } |
|
45 |
|
46 |
|
47 /* method invocation */ |
|
48 |
|
49 object Tag extends Enumeration |
|
50 { |
|
51 val NULL, OK, ERROR, FAIL, INTERRUPT = Value |
|
52 } |
|
53 |
|
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) |
|
60 case Exn.Exn(Exn.Interrupt()) => (Tag.INTERRUPT, "") |
|
61 case Exn.Exn(e) => (Tag.ERROR, Exn.message(e)) |
|
62 } |
|
63 case Exn.Exn(e) => (Tag.FAIL, Exn.message(e)) |
|
64 } |
|
65 } |
|
66 |
|
67 |
|
68 /* protocol handler */ |
|
69 |
|
70 class Scala extends Session.Protocol_Handler |
|
71 { |
|
72 private var session: Session = null |
|
73 private var futures = Map.empty[String, Future[Unit]] |
|
74 |
|
75 override def init(init_session: Session): Unit = |
|
76 synchronized { session = init_session } |
|
77 |
|
78 override def exit(): Unit = synchronized |
|
79 { |
|
80 for ((id, future) <- futures) cancel(id, future) |
|
81 futures = Map.empty |
|
82 } |
|
83 |
|
84 private def fulfill(id: String, tag: Scala.Tag.Value, res: String): Unit = |
|
85 synchronized |
|
86 { |
|
87 if (futures.isDefinedAt(id)) { |
|
88 session.protocol_command("Scala.fulfill", id, tag.id.toString, res) |
|
89 futures -= id |
|
90 } |
|
91 } |
|
92 |
|
93 private def cancel(id: String, future: Future[Unit]) |
|
94 { |
|
95 future.cancel |
|
96 fulfill(id, Scala.Tag.INTERRUPT, "") |
|
97 } |
|
98 |
|
99 private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
|
100 { |
|
101 msg.properties match { |
|
102 case Markup.Invoke_Scala(name, id) => |
|
103 futures += (id -> |
|
104 Future.fork { |
|
105 val (tag, result) = Scala.method(name, msg.text) |
|
106 fulfill(id, tag, result) |
|
107 }) |
|
108 true |
|
109 case _ => false |
|
110 } |
|
111 } |
|
112 |
|
113 private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized |
|
114 { |
|
115 msg.properties match { |
|
116 case Markup.Cancel_Scala(id) => |
|
117 futures.get(id) match { |
|
118 case Some(future) => cancel(id, future) |
|
119 case None => |
|
120 } |
|
121 true |
|
122 case _ => false |
|
123 } |
|
124 } |
|
125 |
|
126 val functions = |
|
127 List( |
|
128 Markup.Invoke_Scala.name -> invoke_scala, |
|
129 Markup.Cancel_Scala.name -> cancel_scala) |
|
130 } |