src/Pure/PIDE/protocol_handlers.scala
author wenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13 ago)
changeset 65214 a2ec0db555c7
child 65215 90a7876d6f4c
permissions -rw-r--r--
clarified modules;
wenzelm@65214
     1
/*  Title:      Pure/PIDE/protocol_handlers.scala
wenzelm@65214
     2
    Author:     Makarius
wenzelm@65214
     3
wenzelm@65214
     4
Management of add-on protocol handlers for PIDE session.
wenzelm@65214
     5
*/
wenzelm@65214
     6
wenzelm@65214
     7
package isabelle
wenzelm@65214
     8
wenzelm@65214
     9
wenzelm@65214
    10
object Protocol_Handlers
wenzelm@65214
    11
{
wenzelm@65214
    12
  private def bad_handler(exn: Throwable, name: String): Unit =
wenzelm@65214
    13
    Output.error_message(
wenzelm@65214
    14
      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
wenzelm@65214
    15
wenzelm@65214
    16
  private val init_state = State()
wenzelm@65214
    17
wenzelm@65214
    18
  sealed case class State(
wenzelm@65214
    19
    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
wenzelm@65214
    20
    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
wenzelm@65214
    21
  {
wenzelm@65214
    22
    def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
wenzelm@65214
    23
wenzelm@65214
    24
    def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State =
wenzelm@65214
    25
    {
wenzelm@65214
    26
      val name = handler.getClass.getName
wenzelm@65214
    27
wenzelm@65214
    28
      val (handlers1, functions1) =
wenzelm@65214
    29
        handlers.get(name) match {
wenzelm@65214
    30
          case Some(old_handler) =>
wenzelm@65214
    31
            Output.warning("Redefining protocol handler: " + name)
wenzelm@65214
    32
            old_handler.stop(prover)
wenzelm@65214
    33
            (handlers - name, functions -- old_handler.functions.keys)
wenzelm@65214
    34
          case None => (handlers, functions)
wenzelm@65214
    35
        }
wenzelm@65214
    36
wenzelm@65214
    37
      val (handlers2, functions2) =
wenzelm@65214
    38
        try {
wenzelm@65214
    39
          handler.start(session, prover)
wenzelm@65214
    40
wenzelm@65214
    41
          val new_functions =
wenzelm@65214
    42
            for ((a, f) <- handler.functions.toList) yield
wenzelm@65214
    43
              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
wenzelm@65214
    44
wenzelm@65214
    45
          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
wenzelm@65214
    46
          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
wenzelm@65214
    47
wenzelm@65214
    48
          (handlers1 + (name -> handler), functions1 ++ new_functions)
wenzelm@65214
    49
        }
wenzelm@65214
    50
        catch {
wenzelm@65214
    51
          case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
wenzelm@65214
    52
        }
wenzelm@65214
    53
      State(handlers2, functions2)
wenzelm@65214
    54
    }
wenzelm@65214
    55
wenzelm@65214
    56
    def add(session: Session, prover: Prover, name: String): State =
wenzelm@65214
    57
    {
wenzelm@65214
    58
      val new_handler =
wenzelm@65214
    59
        try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
wenzelm@65214
    60
        catch { case exn: Throwable => bad_handler(exn, name); None }
wenzelm@65214
    61
      new_handler match {
wenzelm@65214
    62
        case Some(handler) => add(session, prover, handler)
wenzelm@65214
    63
        case None => this
wenzelm@65214
    64
      }
wenzelm@65214
    65
    }
wenzelm@65214
    66
wenzelm@65214
    67
    def invoke(msg: Prover.Protocol_Output): Boolean =
wenzelm@65214
    68
      msg.properties match {
wenzelm@65214
    69
        case Markup.Function(a) if functions.isDefinedAt(a) =>
wenzelm@65214
    70
          try { functions(a)(msg) }
wenzelm@65214
    71
          catch {
wenzelm@65214
    72
            case exn: Throwable =>
wenzelm@65214
    73
              Output.error_message(
wenzelm@65214
    74
                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
wenzelm@65214
    75
            false
wenzelm@65214
    76
          }
wenzelm@65214
    77
        case _ => false
wenzelm@65214
    78
      }
wenzelm@65214
    79
wenzelm@65214
    80
    def stop(prover: Prover): State =
wenzelm@65214
    81
    {
wenzelm@65214
    82
      for ((_, handler) <- handlers) handler.stop(prover)
wenzelm@65214
    83
      init_state
wenzelm@65214
    84
    }
wenzelm@65214
    85
  }
wenzelm@65214
    86
wenzelm@65214
    87
  def init(): Protocol_Handlers = new Protocol_Handlers()
wenzelm@65214
    88
}
wenzelm@65214
    89
wenzelm@65214
    90
class Protocol_Handlers private()
wenzelm@65214
    91
{
wenzelm@65214
    92
  private val state = Synchronized(Protocol_Handlers.init_state)
wenzelm@65214
    93
wenzelm@65214
    94
  def get(name: String): Option[Session.Protocol_Handler] =
wenzelm@65214
    95
    state.value.get(name)
wenzelm@65214
    96
wenzelm@65214
    97
  def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit =
wenzelm@65214
    98
    state.change(_.add(session, prover, handler))
wenzelm@65214
    99
wenzelm@65214
   100
  def add(session: Session, prover: Prover, name: String): Unit =
wenzelm@65214
   101
    state.change(_.add(session, prover, name))
wenzelm@65214
   102
wenzelm@65214
   103
  def invoke(msg: Prover.Protocol_Output): Boolean =
wenzelm@65214
   104
    state.value.invoke(msg)
wenzelm@65214
   105
wenzelm@65214
   106
  def stop(prover: Prover): Unit =
wenzelm@65214
   107
    state.change(_.stop(prover))
wenzelm@65214
   108
}