src/Pure/PIDE/protocol_handlers.scala
author wenzelm
Sun Mar 10 14:19:30 2019 +0100 (4 months ago ago)
changeset 70070 be04e9a053a7
parent 65315 c7097ccbffb7
permissions -rw-r--r--
markup and document markers for some meta data from "Dublin Core Metadata Element Set";
     1 /*  Title:      Pure/PIDE/protocol_handlers.scala
     2     Author:     Makarius
     3 
     4 Management of add-on protocol handlers for PIDE session.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object Protocol_Handlers
    11 {
    12   private def bad_handler(exn: Throwable, name: String): Unit =
    13     Output.error_message(
    14       "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    15 
    16   sealed case class State(
    17     session: Session,
    18     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    19     functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    20   {
    21     def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
    22 
    23     def init(handler: Session.Protocol_Handler): State =
    24     {
    25       val name = handler.getClass.getName
    26 
    27       val (handlers1, functions1) =
    28         handlers.get(name) match {
    29           case Some(old_handler) =>
    30             Output.warning("Redefining protocol handler: " + name)
    31             old_handler.exit()
    32             (handlers - name, functions -- old_handler.functions.map(_._1))
    33           case None => (handlers, functions)
    34         }
    35 
    36       val (handlers2, functions2) =
    37         try {
    38           handler.init(session)
    39 
    40           val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
    41           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    42 
    43           (handlers1 + (name -> handler), functions1 ++ handler.functions)
    44         }
    45         catch {
    46           case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
    47         }
    48       copy(handlers = handlers2, functions = functions2)
    49     }
    50 
    51     def init(name: String): State =
    52     {
    53       val new_handler =
    54         try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    55         catch { case exn: Throwable => bad_handler(exn, name); None }
    56       new_handler match { case Some(handler) => init(handler) case None => this }
    57     }
    58 
    59     def invoke(msg: Prover.Protocol_Output): Boolean =
    60       msg.properties match {
    61         case Markup.Function(a) if functions.isDefinedAt(a) =>
    62           try { functions(a)(msg) }
    63           catch {
    64             case exn: Throwable =>
    65               Output.error_message(
    66                 "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    67             false
    68           }
    69         case _ => false
    70       }
    71 
    72     def exit(): State =
    73     {
    74       for ((_, handler) <- handlers) handler.exit()
    75       copy(handlers = Map.empty, functions = Map.empty)
    76     }
    77   }
    78 
    79   def init(session: Session): Protocol_Handlers =
    80     new Protocol_Handlers(session)
    81 }
    82 
    83 class Protocol_Handlers private(session: Session)
    84 {
    85   private val state = Synchronized(Protocol_Handlers.State(session))
    86 
    87   def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
    88   def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
    89   def init(name: String): Unit = state.change(_.init(name))
    90   def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
    91   def exit(): Unit = state.change(_.exit())
    92 }