author | wenzelm |
Sat, 15 Aug 2020 13:37:34 +0200 | |
changeset 72156 | 065dcd80293e |
parent 71970 | 67fb92378224 |
child 72216 | 0d7cd97f6c48 |
permissions | -rw-r--r-- |
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, |
71970 | 19 |
functions: Map[String, Session.Protocol_Function] = Map.empty) |
65214 | 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 |
|
72156
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
26 |
try { |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
27 |
if (handlers.isDefinedAt(name)) error("Duplicate protocol handler: " + name) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
28 |
else { |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
29 |
handler.init(session) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
30 |
val dups = for ((a, _) <- handler.functions if functions.isDefinedAt(a)) yield a |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
31 |
if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
32 |
copy(handlers = handlers + (name -> handler), functions = functions ++ handler.functions) |
65214 | 33 |
} |
72156
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
34 |
} |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
35 |
catch { case exn: Throwable => bad_handler(exn, name); this } |
65214 | 36 |
} |
37 |
||
65315 | 38 |
def init(name: String): State = |
65214 | 39 |
{ |
40 |
val new_handler = |
|
71734 | 41 |
try { |
42 |
Some(Class.forName(name).getDeclaredConstructor().newInstance() |
|
43 |
.asInstanceOf[Session.Protocol_Handler]) |
|
44 |
} |
|
65214 | 45 |
catch { case exn: Throwable => bad_handler(exn, name); None } |
65315 | 46 |
new_handler match { case Some(handler) => init(handler) case None => this } |
65214 | 47 |
} |
48 |
||
49 |
def invoke(msg: Prover.Protocol_Output): Boolean = |
|
50 |
msg.properties match { |
|
71673 | 51 |
case (Markup.FUNCTION, a) :: _ if functions.isDefinedAt(a) => |
65214 | 52 |
try { functions(a)(msg) } |
53 |
catch { |
|
54 |
case exn: Throwable => |
|
55 |
Output.error_message( |
|
56 |
"Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)) |
|
57 |
false |
|
58 |
} |
|
59 |
case _ => false |
|
60 |
} |
|
61 |
||
65219 | 62 |
def exit(): State = |
65214 | 63 |
{ |
65219 | 64 |
for ((_, handler) <- handlers) handler.exit() |
65215 | 65 |
copy(handlers = Map.empty, functions = Map.empty) |
65214 | 66 |
} |
67 |
} |
|
68 |
||
65215 | 69 |
def init(session: Session): Protocol_Handlers = |
70 |
new Protocol_Handlers(session) |
|
65214 | 71 |
} |
72 |
||
65215 | 73 |
class Protocol_Handlers private(session: Session) |
65214 | 74 |
{ |
65215 | 75 |
private val state = Synchronized(Protocol_Handlers.State(session)) |
65214 | 76 |
|
65219 | 77 |
def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name) |
65315 | 78 |
def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler)) |
79 |
def init(name: String): Unit = state.change(_.init(name)) |
|
65219 | 80 |
def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg) |
81 |
def exit(): Unit = state.change(_.exit()) |
|
65214 | 82 |
} |