Preferences/ConfigurationPages/EditorStylesPage.py

changeset 6648
c09e6c6006eb
parent 6645
ad476851d7e0
child 6842
c83dcb7c6147
--- 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()):

eric ide

mercurial