65214
|
1 |
/* Title: Pure/PIDE/protocol_handlers.scala
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Management of add-on protocol handlers for PIDE session.
|
|
5 |
*/
|
|
6 |
|
|
7 |
package isabelle
|
|
8 |
|
|
9 |
|
|
10 |
object Protocol_Handlers
|
|
11 |
{
|
|
12 |
private def bad_handler(exn: Throwable, name: String): Unit =
|
|
13 |
Output.error_message(
|
|
14 |
"Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
|
|
15 |
|
|
16 |
sealed case class State(
|
65215
|
17 |
session: Session,
|
65214
|
18 |
handlers: Map[String, Session.Protocol_Handler] = Map.empty,
|
|
19 |
functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
|
|
20 |
{
|
|
21 |
def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
|
|
22 |
|
65315
|
23 |
def init(handler: Session.Protocol_Handler): State =
|
65214
|
24 |
{
|
|
25 |
val name = handler.getClass.getName
|
|
26 |
|
|
27 |
val (handlers1, functions1) =
|
|
28 |
handlers.get(name) match {
|
|
29 |
case Some(old_handler) =>
|
|
30 |
Output.warning("Redefining protocol handler: " + name)
|
65219
|
31 |
old_handler.exit()
|
|
32 |
(handlers - name, functions -- old_handler.functions.map(_._1))
|
65214
|
33 |
case None => (handlers, functions)
|
|
34 |
}
|
|
35 |
|
|
36 |
val (handlers2, functions2) =
|
|
37 |
try {
|
65219
|
38 |
handler.init(session)
|
65214
|
39 |
|
65219
|
40 |
val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
|
65214
|
41 |
if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
|
|
42 |
|
65219
|
43 |
(handlers1 + (name -> handler), functions1 ++ handler.functions)
|
65214
|
44 |
}
|
|
45 |
catch {
|
|
46 |
case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
|
|
47 |
}
|
65215
|
48 |
copy(handlers = handlers2, functions = functions2)
|
65214
|
49 |
}
|
|
50 |
|
65315
|
51 |
def init(name: String): State =
|
65214
|
52 |
{
|
|
53 |
val new_handler =
|
|
54 |
try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
|
|
55 |
catch { case exn: Throwable => bad_handler(exn, name); None }
|
65315
|
56 |
new_handler match { case Some(handler) => init(handler) case None => this }
|
65214
|
57 |
}
|
|
58 |
|
|
59 |
def invoke(msg: Prover.Protocol_Output): Boolean =
|
|
60 |
msg.properties match {
|
|
61 |
case Markup.Function(a) if functions.isDefinedAt(a) =>
|
|
62 |
try { functions(a)(msg) }
|
|
63 |
catch {
|
|
64 |
case exn: Throwable =>
|
|
65 |
Output.error_message(
|
|
66 |
"Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
|
|
67 |
false
|
|
68 |
}
|
|
69 |
case _ => false
|
|
70 |
}
|
|
71 |
|
65219
|
72 |
def exit(): State =
|
65214
|
73 |
{
|
65219
|
74 |
for ((_, handler) <- handlers) handler.exit()
|
65215
|
75 |
copy(handlers = Map.empty, functions = Map.empty)
|
65214
|
76 |
}
|
|
77 |
}
|
|
78 |
|
65215
|
79 |
def init(session: Session): Protocol_Handlers =
|
|
80 |
new Protocol_Handlers(session)
|
65214
|
81 |
}
|
|
82 |
|
65215
|
83 |
class Protocol_Handlers private(session: Session)
|
65214
|
84 |
{
|
65215
|
85 |
private val state = Synchronized(Protocol_Handlers.State(session))
|
65214
|
86 |
|
65219
|
87 |
def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
|
65315
|
88 |
def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
|
|
89 |
def init(name: String): Unit = state.change(_.init(name))
|
65219
|
90 |
def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
|
|
91 |
def exit(): Unit = state.change(_.exit())
|
65214
|
92 |
}
|