src/Pure/PIDE/protocol_handlers.scala
changeset 65315 c7097ccbffb7
parent 65219 ed4b47b8c7dc
child 71673 88dfbc382a3d
--- 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())
 }