# HG changeset patch # User wenzelm # Date 1489437455 -3600 # Node ID a2ec0db555c72209aa08f730140b776ccc68fe0d # Parent 51c0f094dc0290a742f1034815ad2077d3c523fc clarified modules; diff -r 51c0f094dc02 -r a2ec0db555c7 src/Pure/PIDE/protocol_handlers.scala --- /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)) +} diff -r 51c0f094dc02 -r a2ec0db555c7 src/Pure/PIDE/session.scala --- 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 } diff -r 51c0f094dc02 -r a2ec0db555c7 src/Pure/build-jars --- 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