From 6ce3e8f72b0d782965dab46e684ad286f4104ebe Mon Sep 17 00:00:00 2001 From: Tom Tromey Date: Tue, 28 Apr 2015 20:47:44 -0600 Subject: [PATCH] use a monospace font --- gui/source.py | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/gui/source.py b/gui/source.py index 073ea00..1546d6e 100644 --- a/gui/source.py +++ b/gui/source.py @@ -1,4 +1,4 @@ -# Copyright (C) 2012, 2013 Tom Tromey +# Copyright (C) 2012, 2013, 2015 Tom Tromey # This program is free software; you can redistribute it and/or modify # it under the terms of the GNU General Public License as published by @@ -25,7 +25,7 @@ import gui.toplevel import gui.events import os.path -from gi.repository import Gtk, GtkSource, GObject, Gdk, GdkPixbuf +from gi.repository import Gtk, GtkSource, GObject, Gdk, GdkPixbuf, Pango class BufferManager: def __init__(self): @@ -193,6 +193,10 @@ class SourceWindow(Toplevel): self.window = builder.get_object("sourcewindow") self.view = builder.get_object("view") + font_desc = Pango.FontDescription('monospace') + if font_desc: + self.view.modify_font(font_desc) + attrs = GtkSource.MarkAttributes() # FIXME: really we want a little green dot... attrs.set_pixbuf(self._get_pixmap('icons/countpoint-marker.png'))