# HG changeset patch
# User wenzelm
# Date 1489868694 -3600
# Node ID c7097ccbffb78eb4b8c238c8148b9ccb268f64dd
# Parent  944758d6462e15ffd7216887e90d8d011157daf9
clarified signature;

diff -r 944758d6462e -r c7097ccbffb7 src/Pure/PIDE/protocol_handlers.scala
--- a/src/Pure/PIDE/protocol_handlers.scala	Sat Mar 18 20:57:15 2017 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala	Sat Mar 18 21:24:54 2017 +0100
@@ -20,7 +20,7 @@
   {
     def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
 
-    def add(handler: Session.Protocol_Handler): State =
+    def init(handler: Session.Protocol_Handler): State =
     {
       val name = handler.getClass.getName
 
@@ -48,12 +48,12 @@
       copy(handlers = handlers2, functions = functions2)
     }
 
-    def add(name: String): State =
+    def init(name: String): State =
     {
       val new_handler =
         try { Some(Class.forName(name).newInstance.asInstanceOf[Session.Protocol_Handler]) }
         catch { case exn: Throwable => bad_handler(exn, name); None }
-      new_handler match { case Some(handler) => add(handler) case None => this }
+      new_handler match { case Some(handler) => init(handler) case None => this }
     }
 
     def invoke(msg: Prover.Protocol_Output): Boolean =
@@ -85,8 +85,8 @@
   private val state = Synchronized(Protocol_Handlers.State(session))
 
   def get(name: String): Option[Session.Protocol_Handler] = state.value.get(name)
-  def add(handler: Session.Protocol_Handler): Unit = state.change(_.add(handler))
-  def add(name: String): Unit = state.change(_.add(name))
+  def init(handler: Session.Protocol_Handler): Unit = state.change(_.init(handler))
+  def init(name: String): Unit = state.change(_.init(name))
   def invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
   def exit(): Unit = state.change(_.exit())
 }
diff -r 944758d6462e -r c7097ccbffb7 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Mar 18 20:57:15 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Sat Mar 18 21:24:54 2017 +0100
@@ -288,17 +288,17 @@
   def get_protocol_handler(name: String): Option[Session.Protocol_Handler] =
     protocol_handlers.get(name)
 
-  def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
-    protocol_handlers.add(handler)
+  def init_protocol_handler(handler: Session.Protocol_Handler): Unit =
+    protocol_handlers.init(handler)
 
-  def add_protocol_handler(name: String): Unit =
-    protocol_handlers.add(name)
+  def init_protocol_handler(name: String): Unit =
+    protocol_handlers.init(name)
 
 
   /* debugger */
 
   private val debugger_handler = new Debugger.Handler(this)
-  add_protocol_handler(debugger_handler)
+  init_protocol_handler(debugger_handler)
 
   def debugger: Debugger = debugger_handler.debugger
 
@@ -397,7 +397,7 @@
           if (!handled) {
             msg.properties match {
               case Markup.Protocol_Handler(name) if prover.defined =>
-                add_protocol_handler(name)
+                init_protocol_handler(name)
 
               case Protocol.Command_Timing(state_id, timing) if prover.defined =>
                 val message = XML.elem(Markup.STATUS, List(XML.Elem(Markup.Timing(timing), Nil)))
diff -r 944758d6462e -r c7097ccbffb7 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Mar 18 20:57:15 2017 +0100
+++ b/src/Pure/Tools/build.scala	Sat Mar 18 21:24:54 2017 +0100
@@ -223,7 +223,7 @@
           val resources = new Resources(deps(parent))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
-          session.add_protocol_handler(handler)
+          session.init_protocol_handler(handler)
 
           val session_result = Future.promise[Int]