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