src/Tools/jEdit/src/document_model.scala

--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:24:33 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 14 21:26:25 2017 +0100
@@ -182,7 +182,7 @@
             }
         })
     if (changed) {
-      PIDE.options_changed()
+      PIDE.plugin.options_changed()
       PIDE.editor.flush()
     }
   }