Lerking/gdb-gui
1
0
Fork 0
mirror of https://github.com/tromey/gdb-gui.git synced 2025-12-15 23:00:05 +01:00
Code Issues Packages Projects Releases Wiki Activity

put [Default] in default log window title

Browse Source
This commit is contained in:
Tom Tromey
2015-05-03 18:15:11 -06:00
parent c52ea9f922
commit d951a7447b
1 changed files with 10 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
gui/logwindow.py
View File

@@ -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)