|
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 private val init_state = State() |
|
17 |
|
18 sealed case class State( |
|
19 handlers: Map[String, Session.Protocol_Handler] = Map.empty, |
|
20 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) |
|
21 { |
|
22 def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name) |
|
23 |
|
24 def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State = |
|
25 { |
|
26 val name = handler.getClass.getName |
|
27 |
|
28 val (handlers1, functions1) = |
|
29 handlers.get(name) match { |
|
30 case Some(old_handler) => |
|
31 Output.warning("Redefining protocol handler: " + name) |
|
32 old_handler.stop(prover) |
|
33 (handlers - name, functions -- old_handler.functions.keys) |
|
34 case None => (handlers, functions) |
|
35 } |
|
36 |
|
37 val (handlers2, functions2) = |
|
38 try { |
|
39 handler.start(session, prover) |
|
40 |
|
41 val new_functions = |
|
42 for ((a, f) <- handler.functions.toList) yield |
|
43 (a, (msg: Prover.Protocol_Output) => f(prover, msg)) |
|
44 |
|
45 val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a |
|
46 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) |
|
47 |
|
48 (handlers1 + (name -> handler), functions1 ++ new_functions) |
|
49 } |
|
50 catch { |
|
51 case exn: Throwable => bad_handler(exn, name); (handlers1, functions1) |
|
52 } |
|
53 State(handlers2, functions2) |
|
54 } |
|
55 |
|
56 def add(session: Session, prover: Prover, name: String): State = |
|
57 { |
|
58 val new_handler = |
|
59 try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) } |
|
60 catch { case exn: Throwable => bad_handler(exn, name); None } |
|
61 new_handler match { |
|
62 case Some(handler) => add(session, prover, handler) |
|
63 case None => this |
|
64 } |
|
65 } |
|
66 |
|
67 def invoke(msg: Prover.Protocol_Output): Boolean = |
|
68 msg.properties match { |
|
69 case Markup.Function(a) if functions.isDefinedAt(a) => |
|
70 try { functions(a)(msg) } |
|
71 catch { |
|
72 case exn: Throwable => |
|
73 Output.error_message( |
|
74 "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn)) |
|
75 false |
|
76 } |
|
77 case _ => false |
|
78 } |
|
79 |
|
80 def stop(prover: Prover): State = |
|
81 { |
|
82 for ((_, handler) <- handlers) handler.stop(prover) |
|
83 init_state |
|
84 } |
|
85 } |
|
86 |
|
87 def init(): Protocol_Handlers = new Protocol_Handlers() |
|
88 } |
|
89 |
|
90 class Protocol_Handlers private() |
|
91 { |
|
92 private val state = Synchronized(Protocol_Handlers.init_state) |
|
93 |
|
94 def get(name: String): Option[Session.Protocol_Handler] = |
|
95 state.value.get(name) |
|
96 |
|
97 def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit = |
|
98 state.change(_.add(session, prover, handler)) |
|
99 |
|
100 def add(session: Session, prover: Prover, name: String): Unit = |
|
101 state.change(_.add(session, prover, name)) |
|
102 |
|
103 def invoke(msg: Prover.Protocol_Output): Boolean = |
|
104 state.value.invoke(msg) |
|
105 |
|
106 def stop(prover: Prover): Unit = |
|
107 state.change(_.stop(prover)) |
|
108 } |