src/Pure/PIDE/protocol_handlers.scala
author wenzelm
Tue Mar 14 00:09:15 2017 +0100 (2017-03-14 ago)
changeset 65219 ed4b47b8c7dc
parent 65215 90a7876d6f4c
child 65315 c7097ccbffb7
permissions -rw-r--r--
misc tuning and simplification;
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
  sealed case class State(
wenzelm@65215
    17
    session: Session,
wenzelm@65214
    18
    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
wenzelm@65214
    19
    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
wenzelm@65214
    20
  {
wenzelm@65214
    21
    def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
wenzelm@65214
    22
wenzelm@65219
    23
    def add(handler: Session.Protocol_Handler): State =
wenzelm@65214
    24
    {
wenzelm@65214
    25
      val name = handler.getClass.getName
wenzelm@65214
    26
wenzelm@65214
    27
      val (handlers1, functions1) =
wenzelm@65214
    28
        handlers.get(name) match {
wenzelm@65214
    29
          case Some(old_handler) =>
wenzelm@65214
    30
            Output.warning("Redefining protocol handler: " + name)
wenzelm@65219
    31
            old_handler.exit()
wenzelm@65219
    32
            (handlers - name, functions -- old_handler.functions.map(_._1))
wenzelm@65214
    33
          case None => (handlers, functions)
wenzelm@65214
    34
        }
wenzelm@65214
    35
wenzelm@65214
    36
      val (handlers2, functions2) =
wenzelm@65214
    37
        try {
wenzelm@65219
    38
          handler.init(session)
wenzelm@65214
    39
wenzelm@65219
    40
          val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
wenzelm@65214
    41
          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
wenzelm@65214
    42
wenzelm@65219
    43
          (handlers1 + (name -> handler), functions1 ++ handler.functions)
wenzelm@65214
    44
        }
wenzelm@65214
    45
        catch {
wenzelm@65214
    46
          case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
wenzelm@65214
    47
        }
wenzelm@65215
    48
      copy(handlers = handlers2, functions = functions2)
wenzelm@65214
    49
    }
wenzelm@65214
    50
wenzelm@65219
    51
    def add(name: String): State =
wenzelm@65214
    52
    {
wenzelm@65214
    53
      val new_handler =
wenzelm@65214
    54
        try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
wenzelm@65214
    55
        catch { case exn: Throwable => bad_handler(exn, name); None }
wenzelm@65219
    56
      new_handler match { case Some(handler) => add(handler) case None => this }
wenzelm@65214
    57
    }
wenzelm@65214
    58
wenzelm@65214
    59
    def invoke(msg: Prover.Protocol_Output): Boolean =
wenzelm@65214
    60
      msg.properties match {
wenzelm@65214
    61
        case Markup.Function(a) if functions.isDefinedAt(a) =>
wenzelm@65214
    62
          try { functions(a)(msg) }
wenzelm@65214
    63
          catch {
wenzelm@65214
    64
            case exn: Throwable =>
wenzelm@65214
    65
              Output.error_message(
wenzelm@65214
    66
                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
wenzelm@65214
    67
            false
wenzelm@65214
    68
          }
wenzelm@65214
    69
        case _ => false
wenzelm@65214
    70
      }
wenzelm@65214
    71
wenzelm@65219
    72
    def exit(): State =
wenzelm@65214
    73
    {
wenzelm@65219
    74
      for ((_, handler) <- handlers) handler.exit()
wenzelm@65215
    75
      copy(handlers = Map.empty, functions = Map.empty)
wenzelm@65214
    76
    }
wenzelm@65214
    77
  }
wenzelm@65214
    78
wenzelm@65215
    79
  def init(session: Session): Protocol_Handlers =
wenzelm@65215
    80
    new Protocol_Handlers(session)
wenzelm@65214
    81
}
wenzelm@65214
    82
wenzelm@65215
    83
class Protocol_Handlers private(session: Session)
wenzelm@65214
    84
{
wenzelm@65215
    85
  private val state = Synchronized(Protocol_Handlers.State(session))
wenzelm@65214
    86
wenzelm@65219
    87
  def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
wenzelm@65219
    88
  def add(handler: Session.Protocol_Handler): Unit = state.change(_.add(handler))
wenzelm@65219
    89
  def add(name: String): Unit = state.change(_.add(name))
wenzelm@65219
    90
  def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
wenzelm@65219
    91
  def exit(): Unit = state.change(_.exit())
wenzelm@65214
    92
}