--- a/src/Pure/PIDE/session.scala Wed Jan 14 16:23:33 2015 +0100
+++ b/src/Pure/PIDE/session.scala Wed Jan 14 16:27:19 2015 +0100
@@ -105,7 +105,7 @@
val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
}
- class Protocol_Handlers(
+ private class Protocol_Handlers(
handlers: Map[String, Session.Protocol_Handler] = Map.empty,
functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
{
@@ -237,14 +237,6 @@
resources.base_syntax
- /* protocol handlers */
-
- @volatile private var _protocol_handlers = new Session.Protocol_Handlers()
-
- def protocol_handler(name: String): Option[Session.Protocol_Handler] =
- _protocol_handlers.get(name)
-
-
/* theory files */
def header_edit(name: Document.Node.Name, header: Document.Node.Header): Document.Edit_Text =
@@ -343,6 +335,17 @@
}
+ /* protocol handlers */
+
+ private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
+
+ def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
+ _protocol_handlers.value.get(name)
+
+ def add_protocol_handler(name: String): Unit =
+ _protocol_handlers.change(_.add(prover.get, name))
+
+
/* manager thread */
private val delay_prune = Simple_Thread.delay_first(prune_delay) { manager.send(Prune_History) }
@@ -432,11 +435,11 @@
output match {
case msg: Prover.Protocol_Output =>
- val handled = _protocol_handlers.invoke(msg)
+ val handled = _protocol_handlers.value.invoke(msg)
if (!handled) {
msg.properties match {
case Markup.Protocol_Handler(name) if prover.defined =>
- _protocol_handlers = _protocol_handlers.add(prover.get, name)
+ add_protocol_handler(name)
case Protocol.Command_Timing(state_id, timing) if prover.defined =>
val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
@@ -525,7 +528,7 @@
case Stop =>
if (prover.defined && is_ready) {
- _protocol_handlers = _protocol_handlers.stop(prover.get)
+ _protocol_handlers.change(_.stop(prover.get))
global_state.change(_ => Document.State.init)
phase = Session.Shutdown
prover.get.terminate