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;
     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   private val init_state = State()
    17 
    18   sealed case class State(
    19     handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    20     functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    21   {
    22     def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
    23 
    24     def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State =
    25     {
    26       val name = handler.getClass.getName
    27 
    28       val (handlers1, functions1) =
    29         handlers.get(name) match {
    30           case Some(old_handler) =>
    31             Output.warning("Redefining protocol handler: " + name)
    32             old_handler.stop(prover)
    33             (handlers - name, functions -- old_handler.functions.keys)
    34           case None => (handlers, functions)
    35         }
    36 
    37       val (handlers2, functions2) =
    38         try {
    39           handler.start(session, prover)
    40 
    41           val new_functions =
    42             for ((a, f) <- handler.functions.toList) yield
    43               (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    44 
    45           val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    46           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    47 
    48           (handlers1 + (name -> handler), functions1 ++ new_functions)
    49         }
    50         catch {
    51           case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
    52         }
    53       State(handlers2, functions2)
    54     }
    55 
    56     def add(session: Session, prover: Prover, name: String): State =
    57     {
    58       val new_handler =
    59         try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    60         catch { case exn: Throwable => bad_handler(exn, name); None }
    61       new_handler match {
    62         case Some(handler) => add(session, prover, handler)
    63         case None => this
    64       }
    65     }
    66 
    67     def invoke(msg: Prover.Protocol_Output): Boolean =
    68       msg.properties match {
    69         case Markup.Function(a) if functions.isDefinedAt(a) =>
    70           try { functions(a)(msg) }
    71           catch {
    72             case exn: Throwable =>
    73               Output.error_message(
    74                 "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    75             false
    76           }
    77         case _ => false
    78       }
    79 
    80     def stop(prover: Prover): State =
    81     {
    82       for ((_, handler) <- handlers) handler.stop(prover)
    83       init_state
    84     }
    85   }
    86 
    87   def init(): Protocol_Handlers = new Protocol_Handlers()
    88 }
    89 
    90 class Protocol_Handlers private()
    91 {
    92   private val state = Synchronized(Protocol_Handlers.init_state)
    93 
    94   def get(name: String): Option[Session.Protocol_Handler] =
    95     state.value.get(name)
    96 
    97   def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit =
    98     state.change(_.add(session, prover, handler))
    99 
   100   def add(session: Session, prover: Prover, name: String): Unit =
   101     state.change(_.add(session, prover, name))
   102 
   103   def invoke(msg: Prover.Protocol_Output): Boolean =
   104     state.value.invoke(msg)
   105 
   106   def stop(prover: Prover): Unit =
   107     state.change(_.stop(prover))
   108 }