Preferences/ConfigurationPages/EditorStylesPage.py

changeset 6278
13fd8759f981
parent 6111
d38b38117d83
child 6299
feb3cf2cbde3
--- a/Preferences/ConfigurationPages/EditorStylesPage.py	Sun May 06 15:23:02 2018 +0200
+++ b/Preferences/ConfigurationPages/EditorStylesPage.py	Mon May 07 19:32:49 2018 +0200
@@ -224,6 +224,8 @@
                         self.changeMarkerSavedColorButton,
                         Preferences.getEditorColour)
         
+        self.markerMapRightCheckBox.setChecked(
+            Preferences.getEditor("ShowMarkerMapOnRight"))
         self.initColour("BookmarksMap",
                         self.bookmarksMapButton,
                         Preferences.getEditorColour)
@@ -354,6 +356,10 @@
             "IndentationGuides",
             self.indentguidesCheckBox.isChecked())
         
+        Preferences.setEditor(
+            "ShowMarkerMapOnRight",
+            self.markerMapRightCheckBox.isChecked())
+        
         self.saveColours(Preferences.setEditorColour)
         for key in list(self.editorColours.keys()):
             Preferences.setEditorColour(key, self.editorColours[key])

eric ide

mercurial