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