62 self.filename2 = '' |
61 self.filename2 = '' |
63 |
62 |
64 self.updateInterval = 20 # update every 20 lines |
63 self.updateInterval = 20 # update every 20 lines |
65 |
64 |
66 font = Preferences.getEditorOtherFonts("MonospacedFont") |
65 font = Preferences.getEditorOtherFonts("MonospacedFont") |
67 self.contents.setFontFamily(font.family()) |
66 self.contents.document().setDefaultFont(font) |
68 self.contents.setFontPointSize(font.pointSize()) |
|
69 |
67 |
70 self.highlighter = DiffHighlighter(self.contents.document()) |
68 self.highlighter = DiffHighlighter(self.contents.document()) |
71 |
69 |
72 # connect some of our widgets explicitly |
70 # connect some of our widgets explicitly |
73 self.file1Picker.textChanged.connect(self.__fileChanged) |
71 self.file1Picker.textChanged.connect(self.__fileChanged) |