misc tuning and simplification;

--- a/src/Pure/PIDE/protocol_handlers.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/PIDE/protocol_handlers.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -20,7 +20,7 @@
   {
     def get(name: String): Option[Session.Protocol_Handler] = handlers.get(name)
 
-    def add(prover: Prover, handler: Session.Protocol_Handler): State =
+    def add(handler: Session.Protocol_Handler): State =
     {
       val name = handler.getClass.getName
 
@@ -28,23 +28,19 @@
         handlers.get(name) match {
           case Some(old_handler) =>
             Output.warning("Redefining protocol handler: " + name)
-            old_handler.stop(prover)
-            (handlers - name, functions -- old_handler.functions.keys)
+            old_handler.exit()
+            (handlers - name, functions -- old_handler.functions.map(_._1))
           case None => (handlers, functions)
         }
 
       val (handlers2, functions2) =
         try {
-          handler.start(session, prover)
+          handler.init(session)
 
-          val new_functions =
-            for ((a, f) <- handler.functions.toList) yield
-              (a, (msg: Prover.Protocol_Output) => f(prover, msg))
-
-          val dups = for ((a, _) <- new_functions if functions1.isDefinedAt(a)) yield a
+          val dups = for ((a, _) <- handler.functions if functions1.isDefinedAt(a)) yield a
           if (dups.nonEmpty) error("Duplicate protocol functions: " + commas_quote(dups))
 
-          (handlers1 + (name -> handler), functions1 ++ new_functions)
+          (handlers1 + (name -> handler), functions1 ++ handler.functions)
         }
         catch {
           case exn: Throwable => bad_handler(exn, name); (handlers1, functions1)
@@ -52,15 +48,12 @@
       copy(handlers = handlers2, functions = functions2)
     }
 
-    def add(prover: Prover, name: String): State =
+    def add(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(prover, handler)
-        case None => this
-      }
+      new_handler match { case Some(handler) => add(handler) case None => this }
     }
 
     def invoke(msg: Prover.Protocol_Output): Boolean =
@@ -76,9 +69,9 @@
         case _ => false
       }
 
-    def stop(prover: Prover): State =
+    def exit(): State =
     {
-      for ((_, handler) <- handlers) handler.stop(prover)
+      for ((_, handler) <- handlers) handler.exit()
       copy(handlers = Map.empty, functions = Map.empty)
     }
   }
@@ -91,18 +84,9 @@
 {
   private val state = Synchronized(Protocol_Handlers.State(session))
 
-  def get(name: String): Option[Session.Protocol_Handler] =
-    state.value.get(name)
-
-  def add(prover: Prover, handler: Session.Protocol_Handler): Unit =
-    state.change(_.add(prover, handler))
-
-  def add(prover: Prover, name: String): Unit =
-    state.change(_.add(prover, name))
-
-  def invoke(msg: Prover.Protocol_Output): Boolean =
-    state.value.invoke(msg)
-
-  def stop(prover: Prover): Unit =
-    state.change(_.stop(prover))
+  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 invoke(msg: Prover.Protocol_Output): Boolean = state.value.invoke(msg)
+  def exit(): Unit = state.change(_.exit())
 }

--- a/src/Pure/PIDE/session.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -107,9 +107,9 @@
 
   abstract class Protocol_Handler
   {
-    def start(session: Session, prover: Prover): Unit = {}
-    def stop(prover: Prover): Unit = {}
-    val functions: Map[String, (Prover, Prover.Protocol_Output) => Boolean]
+    def init(session: Session): Unit = {}
+    def exit(): Unit = {}
+    val functions: List[(String, Prover.Protocol_Output => Boolean)]
   }
 }
 
@@ -289,10 +289,10 @@
     protocol_handlers.get(name)
 
   def add_protocol_handler(handler: Session.Protocol_Handler): Unit =
-    protocol_handlers.add(prover.get, handler)
+    protocol_handlers.add(handler)
 
   def add_protocol_handler(name: String): Unit =
-    protocol_handlers.add(prover.get, name)
+    protocol_handlers.add(name)
 
 
   /* manager thread */
@@ -476,7 +476,7 @@
           case Stop =>
             delay_prune.revoke()
             if (prover.defined) {
-              protocol_handlers.stop(prover.get)
+              protocol_handlers.exit()
               global_state.change(_ => Document.State.init)
               prover.get.terminate
             }

--- a/src/Pure/System/invoke_scala.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/System/invoke_scala.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -71,43 +71,47 @@
 
 class Invoke_Scala extends Session.Protocol_Handler
 {
+  private var session: Session = null
   private var futures = Map.empty[String, Future[Unit]]
 
-  private def fulfill(prover: Prover, id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
+  override def init(init_session: Session): Unit =
+    synchronized { session = init_session }
+
+  private def fulfill(id: String, tag: Invoke_Scala.Tag.Value, res: String): Unit =
     synchronized
     {
       if (futures.isDefinedAt(id)) {
-        prover.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
+        session.protocol_command("Invoke_Scala.fulfill", id, tag.toString, res)
         futures -= id
       }
     }
 
-  private def cancel(prover: Prover, id: String, future: Future[Unit])
+  private def cancel(id: String, future: Future[Unit])
   {
     future.cancel
-    fulfill(prover, id, Invoke_Scala.Tag.INTERRUPT, "")
+    fulfill(id, Invoke_Scala.Tag.INTERRUPT, "")
   }
 
-  private def invoke_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
+  private def invoke_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Invoke_Scala(name, id) =>
         futures += (id ->
           Future.fork {
             val (tag, result) = Invoke_Scala.method(name, msg.text)
-            fulfill(prover, id, tag, result)
+            fulfill(id, tag, result)
           })
         true
       case _ => false
     }
   }
 
-  private def cancel_scala(prover: Prover, msg: Prover.Protocol_Output): Boolean = synchronized
+  private def cancel_scala(msg: Prover.Protocol_Output): Boolean = synchronized
   {
     msg.properties match {
       case Markup.Cancel_Scala(id) =>
         futures.get(id) match {
-          case Some(future) => cancel(prover, id, future)
+          case Some(future) => cancel(id, future)
           case None =>
         }
         true
@@ -115,13 +119,14 @@
     }
   }
 
-  override def stop(prover: Prover): Unit = synchronized
+  override def exit(): Unit = synchronized
   {
-    for ((id, future) <- futures) cancel(prover, id, future)
+    for ((id, future) <- futures) cancel(id, future)
     futures = Map.empty
   }
 
-  val functions = Map(
-    Markup.INVOKE_SCALA -> invoke_scala _,
-    Markup.CANCEL_SCALA -> cancel_scala _)
+  val functions =
+    List(
+      Markup.INVOKE_SCALA -> invoke_scala _,
+      Markup.CANCEL_SCALA -> cancel_scala _)
 }

--- a/src/Pure/Tools/build.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/Tools/build.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -816,13 +816,13 @@
       promise
     }
 
-    private def loading_theory(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def loading_theory(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Loading_Theory(name) => progress.theory(session_name, name); true
         case _ => false
       }
 
-    private def build_theories_result(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def build_theories_result(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Build_Theories_Result(id) =>
           pending.change_result(promises =>
@@ -839,11 +839,11 @@
         case _ => false
       }
 
-    override def stop(prover: Prover): Unit =
+    override def exit(): Unit =
       pending.change(promises => { for ((_, promise) <- promises) promise.cancel; Map.empty })
 
     val functions =
-      Map(
+      List(
         Markup.BUILD_THEORIES_RESULT -> build_theories_result _,
         Markup.LOADING_THEORY -> loading_theory _)
   }

--- a/src/Pure/Tools/debugger.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/Tools/debugger.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -120,7 +120,7 @@
     def get_debugger: Option[Debugger] = _debugger_.value
     def the_debugger: Debugger = get_debugger getOrElse error("Debugger not initialized")
 
-    override def start(session: Session, prover: Prover)
+    override def init(session: Session)
     {
       _debugger_.change(
         {
@@ -129,7 +129,7 @@
         })
     }
 
-    private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def debugger_state(msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
         case Markup.Debugger_State(thread_name) =>
@@ -148,7 +148,7 @@
       }
     }
 
-    private def debugger_output(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def debugger_output(msg: Prover.Protocol_Output): Boolean =
     {
       msg.properties match {
         case Markup.Debugger_Output(thread_name) =>
@@ -165,7 +165,7 @@
     }
 
     val functions =
-      Map(
+      List(
         Markup.DEBUGGER_STATE -> debugger_state _,
         Markup.DEBUGGER_OUTPUT -> debugger_output _)
   }

--- a/src/Pure/Tools/print_operation.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/Tools/print_operation.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -24,7 +24,7 @@
 
     def get: List[(String, String)] = print_operations.value
 
-    private def put(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def put(msg: Prover.Protocol_Output): Boolean =
     {
       val ops =
       {
@@ -35,9 +35,9 @@
       true
     }
 
-    override def start(session: Session, prover: Prover): Unit =
-      prover.protocol_command(Markup.PRINT_OPERATIONS)
+    override def init(session: Session): Unit =
+      session.protocol_command(Markup.PRINT_OPERATIONS)
 
-    val functions = Map(Markup.PRINT_OPERATIONS -> put _)
+    val functions = List(Markup.PRINT_OPERATIONS -> put _)
   }
 }

--- a/src/Pure/Tools/simplifier_trace.scala	Mon Mar 13 23:24:20 2017 +0100
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Mar 14 00:09:15 2017 +0100
@@ -290,7 +290,7 @@
   {
     assert(manager.is_active)
 
-    private def cancel(prover: Prover, msg: Prover.Protocol_Output): Boolean =
+    private def cancel(msg: Prover.Protocol_Output): Boolean =
       msg.properties match {
         case Markup.Simp_Trace_Cancel(serial) =>
           manager.send(Cancel(serial))
@@ -299,12 +299,12 @@
           false
       }
 
-    override def stop(prover: Prover) =
+    override def exit() =
     {
       manager.send(Clear_Memory)
       manager.shutdown()
     }
 
-    val functions = Map(Markup.SIMP_TRACE_CANCEL -> cancel _)
+    val functions = List(Markup.SIMP_TRACE_CANCEL -> cancel _)
   }
 }