From d951a7447b0c9b132b25df5b00aea3eff5697d9e Mon Sep 17 00:00:00 2001 From: Tom Tromey Date: Sun, 3 May 2015 18:15:11 -0600 Subject: [PATCH] put [Default] in default log window title --- gui/logwindow.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/gui/logwindow.py b/gui/logwindow.py index 5de5246..a46b1eb 100644 --- a/gui/logwindow.py +++ b/gui/logwindow.py @@ -41,19 +41,21 @@ class LogWindow(gui.toplevel.Toplevel): self.view.modify_font(gui.params.font_manager.get_font()) self.buffer = builder.get_object('buffer') - self.window.set_title('GDB Log @%d' % self.number) + self.update_title() self.window.show() @in_gtk_thread def set_font(self, font): self.view.modify_font(Pango.FontDescription(font_name)) + @in_gtk_thread def deleted(self, *args): if default_log_window == self: default_log_window = None for window in gui.toplevel.state.windows(): if isinstance(window, LogWindow): default_log_window = window + window.update_title() break def _append(self, text): @@ -66,3 +68,10 @@ class LogWindow(gui.toplevel.Toplevel): @in_gtk_thread def set_font(self, pango_font): self.view.modify_font(pango_font) + + @in_gtk_thread + def update_title(self): + title = 'GDB Log @%d' % self.number + if self is default_log_window: + title += ' [Default]' + self.window.set_title(title)