Lerking/gdb-gui
1
0
Fork 0
mirror of https://github.com/tromey/gdb-gui.git synced 2026-01-04 15:40:06 +01:00
Code Issues Packages Projects Releases Wiki Activity

add "set gui font"

Browse Source
This commit is contained in:
Tom Tromey
2015-05-03 17:54:28 -06:00
parent 6ee0bec04a
commit 8ee28d3cef
4 changed files with 69 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files

8
gui/source.py
View File

@@ -220,9 +220,7 @@ class SourceWindow(gui.updatewindow.UpdateWindow):
for name in BUTTON_NAMES:
self.buttons[name] = builder.get_object(name)
font_desc = Pango.FontDescription('monospace')
if font_desc:
self.view.modify_font(font_desc)
self.view.modify_font(gui.params.font_manager.get_font())
attrs = GtkSource.MarkAttributes()
# FIXME: really we want a little green dot...
@@ -289,3 +287,7 @@ class SourceWindow(gui.updatewindow.UpdateWindow):
buffer_manager.release_buffer(old_buffer)
GObject.idle_add(self._do_scroll, buff, srcline - 1)
# self.view.scroll_to_iter(buff.get_iter_at_line(srcline), 0.0)
@in_gtk_thread
def set_font(self, pango_font):
self.view.modify_font(pango_font)