--- 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!
--- 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
}
--- 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() }
}