# HG changeset patch
# User wenzelm
# Date 1439317976 -7200
# Node ID 11a0f333de6f0d6b120cf647790999b62355af03
# Parent  84569dbe1e308db4ca7b7f26c7b996b7e0b4a2d5
tuned signature;

diff -r 84569dbe1e30 -r 11a0f333de6f src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Tue Aug 11 20:28:11 2015 +0200
+++ b/src/Pure/PIDE/session.scala	Tue Aug 11 20:32:56 2015 +0200
@@ -203,7 +203,7 @@
   val syslog_messages = new Session.Outlet[Prover.Output](dispatcher)
   val raw_output_messages = new Session.Outlet[Prover.Output](dispatcher)
   val trace_events = new Session.Outlet[Simplifier_Trace.Event.type](dispatcher)
-  val debugger_updates = new Session.Outlet[Debugger.Update](dispatcher)
+  val debugger_updates = new Session.Outlet[Debugger.Update.type](dispatcher)
 
   val all_messages = new Session.Outlet[Prover.Message](dispatcher)  // potential bottle-neck!
 
diff -r 84569dbe1e30 -r 11a0f333de6f src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Tue Aug 11 20:28:11 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Tue Aug 11 20:32:56 2015 +0200
@@ -67,21 +67,14 @@
 
   /* protocol handler */
 
-  sealed case class Update(thread_names: Set[String])
+  case object Update
 
   class Handler extends Session.Protocol_Handler
   {
-    private var updated = Set.empty[String]
     private val delay_update =
       Simple_Thread.delay_first(global_state.value.session.output_delay) {
-        global_state.value.session.debugger_updates.post(Update(updated))
-        updated = Set.empty
+        global_state.value.session.debugger_updates.post(Update)
       }
-    private def update(name: String)
-    {
-      updated += name
-      delay_update.invoke()
-    }
 
     private def debugger_state(prover: Prover, msg: Prover.Protocol_Output): Boolean =
     {
@@ -97,7 +90,7 @@
             })
           }
           global_state.change(_.update_thread(thread_name, debug_states))
-          update(thread_name)
+          delay_update.invoke()
           true
         case _ => false
       }
@@ -114,7 +107,7 @@
             case List(XML.Elem(Markup(name, props @ Markup.Serial(i)), body)) =>
               val message = XML.Elem(Markup(Markup.message(name), props), body)
               global_state.change(_.add_output(thread_name, i -> message))
-              update(thread_name)
+              delay_update.invoke()
               true
             case _ => false
           }
diff -r 84569dbe1e30 -r 11a0f333de6f src/Tools/jEdit/src/debugger_dockable.scala
--- a/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 20:28:11 2015 +0200
+++ b/src/Tools/jEdit/src/debugger_dockable.scala	Tue Aug 11 20:32:56 2015 +0200
@@ -352,7 +352,7 @@
         Debugger.set_session(PIDE.session)
         GUI_Thread.later { handle_resize() }
 
-      case _: Debugger.Update =>
+      case Debugger.Update =>
         GUI_Thread.later { handle_update() }
     }