update titles when changed

This commit is contained in:
Tom Tromey
2015-05-05 10:25:45 -06:00
parent adc31aa077
commit 2065b4138a
2 changed files with 11 additions and 1 deletions

View File

@@ -167,7 +167,7 @@ class _Title(_StoredParameter):
@in_gdb_thread
def get_set_string(self):
super(_Title, self).get_set_string()
# gui.toplevel.state.set_font(self.value)
gui.toplevel.state.update_titles()
return ""
_SetBase()

View File

@@ -73,6 +73,16 @@ class _ToplevelState(object):
def set_font(self, font_name):
gui.startup.send_to_gtk(lambda: self._do_set_font(font_name))
@in_gtk_thread
def _do_update_titles(self):
with self.toplevel_lock:
for num in self.toplevels:
self.toplevels[num].update_title()
@in_gdb_thread
def update_titles(self):
gui.startup.send_to_gtk(lambda: self._do_update_titles))
@in_gtk_thread
def windows(self):
return self.toplevels.values()