clarified signature;
authorwenzelm
Sat Mar 18 21:24:54 2017 +0100 (2017-03-18 ago)
changeset 65315c7097ccbffb7
parent 65314 944758d6462e
child 65316 c0fb8405416c
clarified signature;
src/Pure/PIDE/protocol_handlers.scala
src/Pure/PIDE/session.scala
src/Pure/Tools/build.scala
     1.1 --- a/src/Pure/PIDE/protocol_handlers.scala	Sat Mar 18 20:57:15 2017 +0100
     1.2 +++ b/src/Pure/PIDE/protocol_handlers.scala	Sat Mar 18 21:24:54 2017 +0100
     1.3 @@ -20,7 +20,7 @@
     1.4    {
     1.5      def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
     1.6  
     1.7 -    def add(handler: Session.Protocol_Handler): State =
     1.8 +    def init(handler: Session.Protocol_Handler): State =
     1.9      {
    1.10        val name = handler.getClass.getName
    1.11  
    1.12 @@ -48,12 +48,12 @@
    1.13        copy(handlers = handlers2, functions = functions2)
    1.14      }
    1.15  
    1.16 -    def add(name: String): State =
    1.17 +    def init(name: String): State =
    1.18      {
    1.19        val new_handler =
    1.20          try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
    1.21          catch { case exn: Throwable => bad_handler(exn, name); None }
    1.22 -      new_handler match { case Some(handler) => add(handler) case None => this }
    1.23 +      new_handler match { case Some(handler) => init(handler) case None => this }
    1.24      }
    1.25  
    1.26      def invoke(msg: Prover.Protocol_Output): Boolean =
    1.27 @@ -85,8 +85,8 @@
    1.28    private val state = Synchronized(Protocol_Handlers.State(session))
    1.29  
    1.30    def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
    1.31 -  def add(handler: Session.Protocol_Handler): Unit = state.change(_.add(handler))
    1.32 -  def add(name: String): Unit = state.change(_.add(name))
    1.33 +  def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
    1.34 +  def init(name: String): Unit = state.change(_.init(name))
    1.35    def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
    1.36    def exit(): Unit = state.change(_.exit())
    1.37  }
     2.1 --- a/src/Pure/PIDE/session.scala	Sat Mar 18 20:57:15 2017 +0100
     2.2 +++ b/src/Pure/PIDE/session.scala	Sat Mar 18 21:24:54 2017 +0100
     2.3 @@ -288,17 +288,17 @@
     2.4    def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
     2.5      protocol_handlers.get(name)
     2.6  
     2.7 -  def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
     2.8 -    protocol_handlers.add(handler)
     2.9 +  def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
    2.10 +    protocol_handlers.init(handler)
    2.11  
    2.12 -  def add_protocol_handler(name: String): Unit =
    2.13 -    protocol_handlers.add(name)
    2.14 +  def init_protocol_handler(name: String): Unit =
    2.15 +    protocol_handlers.init(name)
    2.16  
    2.17  
    2.18    /* debugger */
    2.19  
    2.20    private val debugger_handler = new Debugger.Handler(this)
    2.21 -  add_protocol_handler(debugger_handler)
    2.22 +  init_protocol_handler(debugger_handler)
    2.23  
    2.24    def debugger: Debugger = debugger_handler.debugger
    2.25  
    2.26 @@ -397,7 +397,7 @@
    2.27            if (!handled) {
    2.28              msg.properties match {
    2.29                case Markup.Protocol_Handler(name) if prover.defined =>
    2.30 -                add_protocol_handler(name)
    2.31 +                init_protocol_handler(name)
    2.32  
    2.33                case Protocol.Command_Timing(state_id, timing) if prover.defined =>
    2.34                  val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
     3.1 --- a/src/Pure/Tools/build.scala	Sat Mar 18 20:57:15 2017 +0100
     3.2 +++ b/src/Pure/Tools/build.scala	Sat Mar 18 21:24:54 2017 +0100
     3.3 @@ -223,7 +223,7 @@
     3.4            val resources = new Resources(deps(parent))
     3.5            val session = new Session(options, resources)
     3.6            val handler = new Handler(progress, session, name)
     3.7 -          session.add_protocol_handler(handler)
     3.8 +          session.init_protocol_handler(handler)
     3.9  
    3.10            val session_result = Future.promise[Int]
    3.11