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

add parameters for line numbers and tab width

Browse Source
This commit is contained in:
Tom Tromey
2015-05-07 11:30:14 -06:00
parent 7956c96cae
commit f94c64d369
4 changed files with 126 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
gui/source.py
View File

@@ -224,6 +224,8 @@ class SourceWindow(gui.updatewindow.UpdateWindow):
self.buttons[name] = builder.get_object(name)
self.view.modify_font(gui.params.font_manager.get_font())
self.view.set_show_line_numbers(gui.params.line_numbers.value)
self.view.set_tab_width(gui.params.tab_width.value)
attrs = GtkSource.MarkAttributes()
# FIXME: really we want a little green dot...
@@ -294,3 +296,11 @@ class SourceWindow(gui.updatewindow.UpdateWindow):
@in_gtk_thread
def set_font(self, pango_font):
self.view.modify_font(pango_font)
@in_gtk_thread
def set_line_numbers(self, want_lines):
self.view.set_show_line_numbers(want_lines)
@in_gtk_thread
def set_tab_width(self, width):
self.view.set_tab_width(width)