tuned signature;
authorwenzelm
Mon Mar 13 22:02:42 2017 +0100 (2017-03-13 ago)
changeset 6521590a7876d6f4c
parent 65214 a2ec0db555c7
child 65216 060a8a1f2dec
tuned signature;
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/protocol_handlers.scala	Mon Mar 13 21:37:35 2017 +0100
     1.2 +++ b/src/Pure/PIDE/protocol_handlers.scala	Mon Mar 13 22:02:42 2017 +0100
     1.3 @@ -13,15 +13,14 @@
     1.4      Output.error_message(
     1.5        "Failed to initialize protocol handler: " + quote(name) + "\n" + Exn.message(exn))
     1.6  
     1.7 -  private val init_state = State()
     1.8 -
     1.9    sealed case class State(
    1.10 +    session: Session,
    1.11      handlers: Map[String, Session.Protocol_Handler] = Map.empty,
    1.12      functions: Map[String, Prover.Protocol_Output => Boolean] = Map.empty)
    1.13    {
    1.14      def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
    1.15  
    1.16 -    def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): State =
    1.17 +    def add(prover: Prover, handler: Session.Protocol_Handler): State =
    1.18      {
    1.19        val name = handler.getClass.getName
    1.20  
    1.21 @@ -50,16 +49,16 @@
    1.22          catch {
    1.23            case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
    1.24          }
    1.25 -      State(handlers2, functions2)
    1.26 +      copy(handlers = handlers2, functions = functions2)
    1.27      }
    1.28  
    1.29 -    def add(session: Session, prover: Prover, name: String): State =
    1.30 +    def add(prover: Prover, name: String): State =
    1.31      {
    1.32        val new_handler =
    1.33          try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    1.34          catch { case exn: Throwable => bad_handler(exn, name); None }
    1.35        new_handler match {
    1.36 -        case Some(handler) => add(session, prover, handler)
    1.37 +        case Some(handler) => add(prover, handler)
    1.38          case None => this
    1.39        }
    1.40      }
    1.41 @@ -80,25 +79,26 @@
    1.42      def stop(prover: Prover): State =
    1.43      {
    1.44        for ((_, handler) <- handlers) handler.stop(prover)
    1.45 -      init_state
    1.46 +      copy(handlers = Map.empty, functions = Map.empty)
    1.47      }
    1.48    }
    1.49  
    1.50 -  def init(): Protocol_Handlers = new Protocol_Handlers()
    1.51 +  def init(session: Session): Protocol_Handlers =
    1.52 +    new Protocol_Handlers(session)
    1.53  }
    1.54  
    1.55 -class Protocol_Handlers private()
    1.56 +class Protocol_Handlers private(session: Session)
    1.57  {
    1.58 -  private val state = Synchronized(Protocol_Handlers.init_state)
    1.59 +  private val state = Synchronized(Protocol_Handlers.State(session))
    1.60  
    1.61    def get(name: String): Option[Session.Protocol_Handler] =
    1.62      state.value.get(name)
    1.63  
    1.64 -  def add(session: Session, prover: Prover, handler: Session.Protocol_Handler): Unit =
    1.65 -    state.change(_.add(session, prover, handler))
    1.66 +  def add(prover: Prover, handler: Session.Protocol_Handler): Unit =
    1.67 +    state.change(_.add(prover, handler))
    1.68  
    1.69 -  def add(session: Session, prover: Prover, name: String): Unit =
    1.70 -    state.change(_.add(session, prover, name))
    1.71 +  def add(prover: Prover, name: String): Unit =
    1.72 +    state.change(_.add(prover, name))
    1.73  
    1.74    def invoke(msg: Prover.Protocol_Output): Boolean =
    1.75      state.value.invoke(msg)
     2.1 --- a/src/Pure/PIDE/session.scala	Mon Mar 13 21:37:35 2017 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Mon Mar 13 22:02:42 2017 +0100
     2.3 @@ -281,16 +281,16 @@
     2.4  
     2.5    /* protocol handlers */
     2.6  
     2.7 -  private val protocol_handlers = Protocol_Handlers.init()
     2.8 +  private val protocol_handlers = Protocol_Handlers.init(session)
     2.9  
    2.10    def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
    2.11      protocol_handlers.get(name)
    2.12  
    2.13    def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
    2.14 -    protocol_handlers.add(session, prover.get, handler)
    2.15 +    protocol_handlers.add(prover.get, handler)
    2.16  
    2.17    def add_protocol_handler(name: String): Unit =
    2.18 -    protocol_handlers.add(session, prover.get, name)
    2.19 +    protocol_handlers.add(prover.get, name)
    2.20  
    2.21  
    2.22    /* manager thread */