# HG changeset patch
# User wenzelm
# Date 1440325671 -7200
# Node ID b88b8227e1a390918af3eb30bc34a083e749adce
# Parent  eaceb601a8a2bb51c7d5096f31ac265900a46b22
proper GUI event;

diff -r eaceb601a8a2 -r b88b8227e1a3 src/Pure/Tools/debugger.scala
--- a/src/Pure/Tools/debugger.scala	Sun Aug 23 12:10:14 2015 +0200
+++ b/src/Pure/Tools/debugger.scala	Sun Aug 23 12:27:51 2015 +0200
@@ -192,8 +192,11 @@
     })
   }
 
-  def set_focus(focus: Option[Position.T]): Unit =
+  def set_focus(focus: Option[Position.T])
+  {
     global_state.change(_.set_focus(focus))
+    delay_update.invoke()
+  }
 
   def threads(): Map[String, List[Debug_State]] = global_state.value.threads