--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/protocol_handlers.scala Mon Mar 13 21:37:35 2017 +0100
@@ -0,0 +1,108 @@
+/* Title: Pure/PIDE/protocol_handlers.scala
+ Author: Makarius
+
+Management of add-on protocol handlers for PIDE session.
+*/
+
+package isabelle
+
+
+object Protocol_Handlers
+{
+ private def bad_handler(exn: Throwable, name: String): Unit =
+ Output.error_message(
+ "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
+
+ private val init_state = State()
+
+ sealed case class State(
+ handlers: Map[String, Session.Protocol_Handler] = Map.empty,
+ functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
+ {
+ def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
+
+ def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State =
+ {
+ val name = handler.getClass.getName
+
+ val (handlers1, functions1) =
+ handlers.get(name) match {
+ case Some(old_handler) =>
+ Output.warning("Redefining protocol handler: " + name)
+ old_handler.stop(prover)
+ (handlers - name, functions -- old_handler.functions.keys)
+ case None => (handlers, functions)
+ }
+
+ val (handlers2, functions2) =
+ try {
+ handler.start(session, prover)
+
+ val new_functions =
+ for ((a, f) <- handler.functions.toList) yield
+ (a, (msg: Prover.Protocol_Output) => f(prover, msg))
+
+ val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
+ if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
+
+ (handlers1 + (name -> handler), functions1 ++ new_functions)
+ }
+ catch {
+ case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
+ }
+ State(handlers2, functions2)
+ }
+
+ def add(session: Session, prover: Prover, name: String): State =
+ {
+ val new_handler =
+ try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
+ catch { case exn: Throwable => bad_handler(exn, name); None }
+ new_handler match {
+ case Some(handler) => add(session, prover, handler)
+ case None => this
+ }
+ }
+
+ def invoke(msg: Prover.Protocol_Output): Boolean =
+ msg.properties match {
+ case Markup.Function(a) if functions.isDefinedAt(a) =>
+ try { functions(a)(msg) }
+ catch {
+ case exn: Throwable =>
+ Output.error_message(
+ "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
+ false
+ }
+ case _ => false
+ }
+
+ def stop(prover: Prover): State =
+ {
+ for ((_, handler) <- handlers) handler.stop(prover)
+ init_state
+ }
+ }
+
+ def init(): Protocol_Handlers = new Protocol_Handlers()
+}
+
+class Protocol_Handlers private()
+{
+ private val state = Synchronized(Protocol_Handlers.init_state)
+
+ def get(name: String): Option[Session.Protocol_Handler] =
+ state.value.get(name)
+
+ def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit =
+ state.change(_.add(session, prover, handler))
+
+ def add(session: Session, prover: Prover, name: String): Unit =
+ state.change(_.add(session, prover, name))
+
+ def invoke(msg: Prover.Protocol_Output): Boolean =
+ state.value.invoke(msg)
+
+ def stop(prover: Prover): Unit =
+ state.change(_.stop(prover))
+}
--- a/src/Pure/PIDE/session.scala Mon Mar 13 20:33:42 2017 +0100
+++ b/src/Pure/PIDE/session.scala Mon Mar 13 21:37:35 2017 +0100
@@ -111,76 +111,14 @@
def stop(prover: Prover): Unit = {}
val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
}
-
- def bad_protocol_handler(exn: Throwable, name: String): Unit =
- Output.error_message(
- "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
-
- private class Protocol_Handlers(
- handlers: Map[String, Session.Protocol_Handler] = Map.empty,
- functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
- {
- def get(name: String): Option[Protocol_Handler] = handlers.get(name)
-
- def add(session: Session, prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
- {
- val name = handler.getClass.getName
-
- val (handlers1, functions1) =
- handlers.get(name) match {
- case Some(old_handler) =>
- Output.warning("Redefining protocol handler: " + name)
- old_handler.stop(prover)
- (handlers - name, functions -- old_handler.functions.keys)
- case None => (handlers, functions)
- }
-
- val (handlers2, functions2) =
- try {
- handler.start(session, prover)
-
- val new_functions =
- for ((a, f) <- handler.functions.toList) yield
- (a, (msg: Prover.Protocol_Output) => f(prover, msg))
-
- val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
- if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
-
- (handlers1 + (name -> handler), functions1 ++ new_functions)
- }
- catch {
- case exn: Throwable =>
- Session.bad_protocol_handler(exn, name)
- (handlers1, functions1)
- }
-
- new Protocol_Handlers(handlers2, functions2)
- }
-
- def invoke(msg: Prover.Protocol_Output): Boolean =
- msg.properties match {
- case Markup.Function(a) if functions.isDefinedAt(a) =>
- try { functions(a)(msg) }
- catch {
- case exn: Throwable =>
- Output.error_message(
- "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
- false
- }
- case _ => false
- }
-
- def stop(prover: Prover): Protocol_Handlers =
- {
- for ((_, handler) <- handlers) handler.stop(prover)
- new Protocol_Handlers()
- }
- }
}
class Session(val resources: Resources)
{
+ session =>
+
+
/* global flags */
@volatile var timing: Boolean = false
@@ -343,13 +281,16 @@
/* protocol handlers */
- private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
+ private val protocol_handlers = Protocol_Handlers.init()
def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
- _protocol_handlers.value.get(name)
+ protocol_handlers.get(name)
def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
- _protocol_handlers.change(_.add(this, prover.get, handler))
+ protocol_handlers.add(session, prover.get, handler)
+
+ def add_protocol_handler(name: String): Unit =
+ protocol_handlers.add(session, prover.get, name)
/* manager thread */
@@ -442,16 +383,11 @@
output match {
case msg: Prover.Protocol_Output =>
- val handled = _protocol_handlers.value.invoke(msg)
+ val handled = protocol_handlers.invoke(msg)
if (!handled) {
msg.properties match {
case Markup.Protocol_Handler(name) if prover.defined =>
- try {
- val handler =
- Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]
- add_protocol_handler(handler)
- }
- catch { case exn: Throwable => Session.bad_protocol_handler(exn, 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)))
@@ -538,7 +474,7 @@
case Stop =>
delay_prune.revoke()
if (prover.defined) {
- _protocol_handlers.change(_.stop(prover.get))
+ protocol_handlers.stop(prover.get)
global_state.change(_ => Document.State.init)
prover.get.terminate
}
--- a/src/Pure/build-jars Mon Mar 13 20:33:42 2017 +0100
+++ b/src/Pure/build-jars Mon Mar 13 21:37:35 2017 +0100
@@ -94,6 +94,7 @@
PIDE/markup.scala
PIDE/markup_tree.scala
PIDE/protocol.scala
+ PIDE/protocol_handlers.scala
PIDE/protocol_message.scala
PIDE/prover.scala
PIDE/query_operation.scala