author | wenzelm |
Thu, 04 Mar 2021 15:41:46 +0100 | |
changeset 73359 | d8a0e996614b |
parent 72217 | e35997591c5b |
child 75393 | 87ebf5a50283 |
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 |
{ |
|
72217 | 12 |
private def err_handler(exn: Throwable, name: String): Nothing = |
13 |
error("Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)) |
|
65214 | 14 |
|
15 |
sealed case class State( |
|
65215 | 16 |
session: Session, |
65214 | 17 |
handlers: Map[String, Session.Protocol_Handler] = Map.empty, |
71970 | 18 |
functions: Map[String, Session.Protocol_Function] = Map.empty) |
65214 | 19 |
{ |
20 |
def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name) |
|
21 |
||
65315 | 22 |
def init(handler: Session.Protocol_Handler): State = |
65214 | 23 |
{ |
24 |
val name = handler.getClass.getName |
|
72156
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
25 |
try { |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
26 |
if (handlers.isDefinedAt(name)) error("Duplicate protocol handler: " + name) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
27 |
else { |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
28 |
handler.init(session) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
29 |
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
|
30 |
if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) |
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
31 |
copy(handlers = handlers + (name -> handler), functions = functions ++ handler.functions) |
65214 | 32 |
} |
72156
065dcd80293e
provide protocol handlers via isabelle_system_service;
wenzelm
parents:
71970
diff
changeset
|
33 |
} |
72217 | 34 |
catch { case exn: Throwable => err_handler(exn, name) } |
65214 | 35 |
} |
36 |
||
65315 | 37 |
def init(name: String): State = |
65214 | 38 |
{ |
72217 | 39 |
val handler = |
71734 | 40 |
try { |
72217 | 41 |
Class.forName(name).getDeclaredConstructor().newInstance() |
42 |
.asInstanceOf[Session.Protocol_Handler] |
|
71734 | 43 |
} |
72217 | 44 |
catch { case exn: Throwable => err_handler(exn, name) } |
45 |
init(handler) |
|
65214 | 46 |
} |
47 |
||
48 |
def invoke(msg: Prover.Protocol_Output): Boolean = |
|
49 |
msg.properties match { |
|
71673 | 50 |
case (Markup.FUNCTION, a) :: _ if functions.isDefinedAt(a) => |
65214 | 51 |
try { functions(a)(msg) } |
52 |
catch { |
|
53 |
case exn: Throwable => |
|
54 |
Output.error_message( |
|
55 |
"Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)) |
|
56 |
false |
|
57 |
} |
|
58 |
case _ => false |
|
59 |
} |
|
60 |
||
65219 | 61 |
def exit(): State = |
65214 | 62 |
{ |
65219 | 63 |
for ((_, handler) <- handlers) handler.exit() |
65215 | 64 |
copy(handlers = Map.empty, functions = Map.empty) |
65214 | 65 |
} |
66 |
} |
|
67 |
||
65215 | 68 |
def init(session: Session): Protocol_Handlers = |
69 |
new Protocol_Handlers(session) |
|
65214 | 70 |
} |
71 |
||
65215 | 72 |
class Protocol_Handlers private(session: Session) |
65214 | 73 |
{ |
65215 | 74 |
private val state = Synchronized(Protocol_Handlers.State(session)) |
65214 | 75 |
|
72216 | 76 |
def prover_options(options: Options): Options = |
73359 | 77 |
state.value.handlers.foldLeft(options) { |
78 |
case (opts, (_, handler)) => handler.prover_options(opts) |
|
79 |
} |
|
72216 | 80 |
|
65219 | 81 |
def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name) |
65315 | 82 |
def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler)) |
83 |
def init(name: String): Unit = state.change(_.init(name)) |
|
65219 | 84 |
def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg) |
85 |
def exit(): Unit = state.change(_.exit()) |
|
65214 | 86 |
} |