src/Pure/PIDE/protocol_handlers.scala
changeset 65214 a2ec0db555c7
child 65215 90a7876d6f4c
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/PIDE/protocol_handlers.scala	Mon Mar 13 21:37:35 2017 +0100
     1.3 @@ -0,0 +1,108 @@
     1.4 +/*  Title:      Pure/PIDE/protocol_handlers.scala
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Management of add-on protocol handlers for PIDE session.
     1.8 +*/
     1.9 +
    1.10 +package isabelle
    1.11 +
    1.12 +
    1.13 +object Protocol_Handlers
    1.14 +{
    1.15 +  private def bad_handler(exn: Throwable, name: String): Unit =
    1.16 +    Output.error_message(
    1.17 +      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    1.18 +
    1.19 +  private val init_state = State()
    1.20 +
    1.21 +  sealed case class State(
    1.22 +    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    1.23 +    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    1.24 +  {
    1.25 +    def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
    1.26 +
    1.27 +    def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State =
    1.28 +    {
    1.29 +      val name = handler.getClass.getName
    1.30 +
    1.31 +      val (handlers1, functions1) =
    1.32 +        handlers.get(name) match {
    1.33 +          case Some(old_handler) =>
    1.34 +            Output.warning("Redefining protocol handler: " + name)
    1.35 +            old_handler.stop(prover)
    1.36 +            (handlers - name, functions -- old_handler.functions.keys)
    1.37 +          case None => (handlers, functions)
    1.38 +        }
    1.39 +
    1.40 +      val (handlers2, functions2) =
    1.41 +        try {
    1.42 +          handler.start(session, prover)
    1.43 +
    1.44 +          val new_functions =
    1.45 +            for ((a, f) <- handler.functions.toList) yield
    1.46 +              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    1.47 +
    1.48 +          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    1.49 +          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    1.50 +
    1.51 +          (handlers1 + (name -> handler), functions1 ++ new_functions)
    1.52 +        }
    1.53 +        catch {
    1.54 +          case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
    1.55 +        }
    1.56 +      State(handlers2, functions2)
    1.57 +    }
    1.58 +
    1.59 +    def add(session: Session, prover: Prover, name: String): State =
    1.60 +    {
    1.61 +      val new_handler =
    1.62 +        try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    1.63 +        catch { case exn: Throwable => bad_handler(exn, name); None }
    1.64 +      new_handler match {
    1.65 +        case Some(handler) => add(session, prover, handler)
    1.66 +        case None => this
    1.67 +      }
    1.68 +    }
    1.69 +
    1.70 +    def invoke(msg: Prover.Protocol_Output): Boolean =
    1.71 +      msg.properties match {
    1.72 +        case Markup.Function(a) if functions.isDefinedAt(a) =>
    1.73 +          try { functions(a)(msg) }
    1.74 +          catch {
    1.75 +            case exn: Throwable =>
    1.76 +              Output.error_message(
    1.77 +                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    1.78 +            false
    1.79 +          }
    1.80 +        case _ => false
    1.81 +      }
    1.82 +
    1.83 +    def stop(prover: Prover): State =
    1.84 +    {
    1.85 +      for ((_, handler) <- handlers) handler.stop(prover)
    1.86 +      init_state
    1.87 +    }
    1.88 +  }
    1.89 +
    1.90 +  def init(): Protocol_Handlers = new Protocol_Handlers()
    1.91 +}
    1.92 +
    1.93 +class Protocol_Handlers private()
    1.94 +{
    1.95 +  private val state = Synchronized(Protocol_Handlers.init_state)
    1.96 +
    1.97 +  def get(name: String): Option[Session.Protocol_Handler] =
    1.98 +    state.value.get(name)
    1.99 +
   1.100 +  def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit =
   1.101 +    state.change(_.add(session, prover, handler))
   1.102 +
   1.103 +  def add(session: Session, prover: Prover, name: String): Unit =
   1.104 +    state.change(_.add(session, prover, name))
   1.105 +
   1.106 +  def invoke(msg: Prover.Protocol_Output): Boolean =
   1.107 +    state.value.invoke(msg)
   1.108 +
   1.109 +  def stop(prover: Prover): Unit =
   1.110 +    state.change(_.stop(prover))
   1.111 +}