clarified modules;
authorwenzelm
Mon Mar 13 21:37:35 2017 +0100 (2017-03-13)
changeset 65214a2ec0db555c7
parent 65213 51c0f094dc02
child 65215 90a7876d6f4c
clarified modules;
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/session.scala
src/Pure/build-jars
     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 +}
     2.1 --- a/src/Pure/PIDE/session.scala	Mon Mar 13 20:33:42 2017 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Mon Mar 13 21:37:35 2017 +0100
     2.3 @@ -111,76 +111,14 @@
     2.4      def stop(prover: Prover): Unit = {}
     2.5      val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
     2.6    }
     2.7 -
     2.8 -  def bad_protocol_handler(exn: Throwable, name: String): Unit =
     2.9 -    Output.error_message(
    2.10 -      "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
    2.11 -
    2.12 -  private class Protocol_Handlers(
    2.13 -    handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    2.14 -    functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    2.15 -  {
    2.16 -    def get(name: String): Option[Protocol_Handler] = handlers.get(name)
    2.17 -
    2.18 -    def add(session: Session, prover: Prover, handler: Protocol_Handler): Protocol_Handlers =
    2.19 -    {
    2.20 -      val name = handler.getClass.getName
    2.21 -
    2.22 -      val (handlers1, functions1) =
    2.23 -        handlers.get(name) match {
    2.24 -          case Some(old_handler) =>
    2.25 -            Output.warning("Redefining protocol handler: " + name)
    2.26 -            old_handler.stop(prover)
    2.27 -            (handlers - name, functions -- old_handler.functions.keys)
    2.28 -          case None => (handlers, functions)
    2.29 -        }
    2.30 -
    2.31 -      val (handlers2, functions2) =
    2.32 -        try {
    2.33 -          handler.start(session, prover)
    2.34 -
    2.35 -          val new_functions =
    2.36 -            for ((a, f) <- handler.functions.toList) yield
    2.37 -              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
    2.38 -
    2.39 -          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
    2.40 -          if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
    2.41 -
    2.42 -          (handlers1 + (name -> handler), functions1 ++ new_functions)
    2.43 -        }
    2.44 -        catch {
    2.45 -          case exn: Throwable =>
    2.46 -            Session.bad_protocol_handler(exn, name)
    2.47 -            (handlers1, functions1)
    2.48 -        }
    2.49 -
    2.50 -      new Protocol_Handlers(handlers2, functions2)
    2.51 -    }
    2.52 -
    2.53 -    def invoke(msg: Prover.Protocol_Output): Boolean =
    2.54 -      msg.properties match {
    2.55 -        case Markup.Function(a) if functions.isDefinedAt(a) =>
    2.56 -          try { functions(a)(msg) }
    2.57 -          catch {
    2.58 -            case exn: Throwable =>
    2.59 -              Output.error_message(
    2.60 -                "Failed invocation of protocol function: " + quote(a) + "\n" + Exn.message(exn))
    2.61 -            false
    2.62 -          }
    2.63 -        case _ => false
    2.64 -      }
    2.65 -
    2.66 -    def stop(prover: Prover): Protocol_Handlers =
    2.67 -    {
    2.68 -      for ((_, handler) <- handlers) handler.stop(prover)
    2.69 -      new Protocol_Handlers()
    2.70 -    }
    2.71 -  }
    2.72  }
    2.73  
    2.74  
    2.75  class Session(val resources: Resources)
    2.76  {
    2.77 +  session =>
    2.78 +
    2.79 +
    2.80    /* global flags */
    2.81  
    2.82    @volatile var timing: Boolean = false
    2.83 @@ -343,13 +281,16 @@
    2.84  
    2.85    /* protocol handlers */
    2.86  
    2.87 -  private val _protocol_handlers = Synchronized(new Session.Protocol_Handlers)
    2.88 +  private val protocol_handlers = Protocol_Handlers.init()
    2.89  
    2.90    def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
    2.91 -    _protocol_handlers.value.get(name)
    2.92 +    protocol_handlers.get(name)
    2.93  
    2.94    def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
    2.95 -    _protocol_handlers.change(_.add(this, prover.get, handler))
    2.96 +    protocol_handlers.add(session, prover.get, handler)
    2.97 +
    2.98 +  def add_protocol_handler(name: String): Unit =
    2.99 +    protocol_handlers.add(session, prover.get, name)
   2.100  
   2.101  
   2.102    /* manager thread */
   2.103 @@ -442,16 +383,11 @@
   2.104  
   2.105        output match {
   2.106          case msg: Prover.Protocol_Output =>
   2.107 -          val handled = _protocol_handlers.value.invoke(msg)
   2.108 +          val handled = protocol_handlers.invoke(msg)
   2.109            if (!handled) {
   2.110              msg.properties match {
   2.111                case Markup.Protocol_Handler(name) if prover.defined =>
   2.112 -                try {
   2.113 -                  val handler =
   2.114 -                    Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]
   2.115 -                  add_protocol_handler(handler)
   2.116 -                }
   2.117 -                catch { case exn: Throwable => Session.bad_protocol_handler(exn, name) }
   2.118 +                add_protocol_handler(name)
   2.119  
   2.120                case Protocol.Command_Timing(state_id, timing) if prover.defined =>
   2.121                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
   2.122 @@ -538,7 +474,7 @@
   2.123            case Stop =>
   2.124              delay_prune.revoke()
   2.125              if (prover.defined) {
   2.126 -              _protocol_handlers.change(_.stop(prover.get))
   2.127 +              protocol_handlers.stop(prover.get)
   2.128                global_state.change(_ => Document.State.init)
   2.129                prover.get.terminate
   2.130              }
     3.1 --- a/src/Pure/build-jars	Mon Mar 13 20:33:42 2017 +0100
     3.2 +++ b/src/Pure/build-jars	Mon Mar 13 21:37:35 2017 +0100
     3.3 @@ -94,6 +94,7 @@
     3.4    PIDE/markup.scala
     3.5    PIDE/markup_tree.scala
     3.6    PIDE/protocol.scala
     3.7 +  PIDE/protocol_handlers.scala
     3.8    PIDE/protocol_message.scala
     3.9    PIDE/prover.scala
    3.10    PIDE/query_operation.scala