proper GUI event;
authorwenzelm
Sun, 23 Aug 2015 12:27:51 +0200
changeset 61008 b88b8227e1a3
parent 61007 eaceb601a8a2
child 61009 a9574cdd5eaf
proper GUI event;
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