--- a/Preferences/ConfigurationPages/EditorStylesPage.py Thu Jan 10 14:18:48 2019 +0100 +++ b/Preferences/ConfigurationPages/EditorStylesPage.py Thu Jan 10 18:01:19 2019 +0100 @@ -257,6 +257,12 @@ self.initColour("MarkerMapBackground", self.markerMapBackgroundButton, Preferences.getEditorColour) + self.changesMarkerCheckBox.setChecked( + Preferences.getEditor("ShowMarkerChanges")) + self.coverageMarkerCheckBox.setChecked( + Preferences.getEditor("ShowMarkerCoverage")) + self.searchMarkerCheckBox.setChecked( + Preferences.getEditor("ShowMarkerSearch")) self.indentguidesCheckBox.setChecked( Preferences.getEditor("IndentationGuides")) @@ -355,6 +361,15 @@ Preferences.setEditor( "ShowMarkerMapOnRight", self.markerMapRightCheckBox.isChecked()) + Preferences.setEditor( + "ShowMarkerChanges", + self.changesMarkerCheckBox.isChecked()) + Preferences.setEditor( + "ShowMarkerCoverage", + self.coverageMarkerCheckBox.isChecked()) + Preferences.setEditor( + "ShowMarkerSearch", + self.searchMarkerCheckBox.isChecked()) self.saveColours(Preferences.setEditorColour) for key in list(self.editorColours.keys()):