Add Editor::changePreferredSettings() to fix problems with mini editor

changing the preferred document settings (scroll+zoom).

src/modules/editors.cpp

@@ -127,6 +127,17 @@ public:
 
 };
 
+class MiniEditor : public Editor
+{
+public:
+  MiniEditor() {
+  }
+
+  bool changePreferredSettings() OVERRIDE {
+    return false;
+  }
+};
+
 int init_module_editors()
 {
   return 0;
@@ -553,7 +564,7 @@ static void create_mini_editor_frame()
   View* newView = new EditorView(EditorView::AlwaysSelected);
   jwidget_expansive(newView, true);
 
-  mini_editor = new Editor();
+  mini_editor = new MiniEditor();
   editors.push_back(EditorItem(mini_editor, EditorItem::Mini));
 
   newView->attachToView(mini_editor);

src/widgets/editor/editor.cpp

@@ -205,7 +205,7 @@ void Editor::setEditorScroll(int x, int y, int use_refresh_region)
   view->setViewScroll(Point(x, y));
   Point newScroll = view->getViewScroll();
 
-  if (m_document) {
+  if (m_document && changePreferredSettings()) {
     PreferredEditorSettings preferred;
 
     preferred.virgin = false;

src/widgets/editor/editor.h

@@ -156,6 +156,12 @@ protected:
   bool onProcessMessage(Message* msg) OVERRIDE;
   void onCurrentToolChange();
 
+  // Returns true if this editor should change the preferred document
+  // settings.
+  virtual bool changePreferredSettings() {
+    return true;
+  }
+
 private:
   void drawGrid(const gfx::Rect& gridBounds, const Color& color);