103 def start(prover: Prover): Unit = {} |
103 def start(prover: Prover): Unit = {} |
104 def stop(prover: Prover): Unit = {} |
104 def stop(prover: Prover): Unit = {} |
105 val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean] |
105 val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean] |
106 } |
106 } |
107 |
107 |
|
108 def bad_protocol_handler(exn: Throwable, name: String): Unit = |
|
109 Output.error_message( |
|
110 "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)) |
|
111 |
108 private class Protocol_Handlers( |
112 private class Protocol_Handlers( |
109 handlers: Map[String, Session.Protocol_Handler] = Map.empty, |
113 handlers: Map[String, Session.Protocol_Handler] = Map.empty, |
110 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) |
114 functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty) |
111 { |
115 { |
112 def get(name: String): Option[Protocol_Handler] = handlers.get(name) |
116 def get(name: String): Option[Protocol_Handler] = handlers.get(name) |
113 |
117 |
114 def add(prover: Prover, name: String): Protocol_Handlers = |
118 def add(prover: Prover, handler: Protocol_Handler): Protocol_Handlers = |
115 { |
119 { |
|
120 val name = handler.getClass.getName |
|
121 |
116 val (handlers1, functions1) = |
122 val (handlers1, functions1) = |
117 handlers.get(name) match { |
123 handlers.get(name) match { |
118 case Some(old_handler) => |
124 case Some(old_handler) => |
119 Output.warning("Redefining protocol handler: " + name) |
125 Output.warning("Redefining protocol handler: " + name) |
120 old_handler.stop(prover) |
126 old_handler.stop(prover) |
122 case None => (handlers, functions) |
128 case None => (handlers, functions) |
123 } |
129 } |
124 |
130 |
125 val (handlers2, functions2) = |
131 val (handlers2, functions2) = |
126 try { |
132 try { |
127 val new_handler = Class.forName(name).newInstance.asInstanceOf[Protocol_Handler] |
133 handler.start(prover) |
128 new_handler.start(prover) |
|
129 |
134 |
130 val new_functions = |
135 val new_functions = |
131 for ((a, f) <- new_handler.functions.toList) yield |
136 for ((a, f) <- handler.functions.toList) yield |
132 (a, (msg: Prover.Protocol_Output) => f(prover, msg)) |
137 (a, (msg: Prover.Protocol_Output) => f(prover, msg)) |
133 |
138 |
134 val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a |
139 val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a |
135 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) |
140 if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups)) |
136 |
141 |
137 (handlers1 + (name -> new_handler), functions1 ++ new_functions) |
142 (handlers1 + (name -> handler), functions1 ++ new_functions) |
138 } |
143 } |
139 catch { |
144 catch { |
140 case exn: Throwable => |
145 case exn: Throwable => |
141 Output.error_message( |
146 Session.bad_protocol_handler(exn, name) |
142 "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn)) |
|
143 (handlers1, functions1) |
147 (handlers1, functions1) |
144 } |
148 } |
145 |
149 |
146 new Protocol_Handlers(handlers2, functions2) |
150 new Protocol_Handlers(handlers2, functions2) |
147 } |
151 } |
340 private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers) |
344 private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers) |
341 |
345 |
342 def get_protocol_handler(name: String): Option[Session.Protocol_Handler] = |
346 def get_protocol_handler(name: String): Option[Session.Protocol_Handler] = |
343 _protocol_handlers.value.get(name) |
347 _protocol_handlers.value.get(name) |
344 |
348 |
345 def add_protocol_handler(name: String): Unit = |
349 def add_protocol_handler(handler: Session.Protocol_Handler): Unit = |
346 _protocol_handlers.change(_.add(prover.get, name)) |
350 _protocol_handlers.change(_.add(prover.get, handler)) |
347 |
351 |
348 |
352 |
349 /* manager thread */ |
353 /* manager thread */ |
350 |
354 |
351 private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) } |
355 private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) } |
437 case msg: Prover.Protocol_Output => |
441 case msg: Prover.Protocol_Output => |
438 val handled = _protocol_handlers.value.invoke(msg) |
442 val handled = _protocol_handlers.value.invoke(msg) |
439 if (!handled) { |
443 if (!handled) { |
440 msg.properties match { |
444 msg.properties match { |
441 case Markup.Protocol_Handler(name) if prover.defined => |
445 case Markup.Protocol_Handler(name) if prover.defined => |
442 add_protocol_handler(name) |
446 try { |
|
447 val handler = |
|
448 Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler] |
|
449 add_protocol_handler(handler) |
|
450 } |
|
451 catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) } |
443 |
452 |
444 case Protocol.Command_Timing(state_id, timing) if prover.defined => |
453 case Protocol.Command_Timing(state_id, timing) if prover.defined => |
445 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) |
454 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil))) |
446 accumulate(state_id, prover.get.xml_cache.elem(message)) |
455 accumulate(state_id, prover.get.xml_cache.elem(message)) |
447 |
456 |