--- a/src/Tools/jEdit/src/plugin.scala Thu Feb 04 21:28:56 2016 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Thu Feb 04 21:53:06 2016 +0100
@@ -377,6 +377,15 @@
}
case msg: PropertiesChanged =>
+ for {
+ view <- JEdit_Lib.jedit_views
+ edit_pane <- JEdit_Lib.jedit_edit_panes(view)
+ } {
+ val buffer = edit_pane.getBuffer
+ val text_area = edit_pane.getTextArea
+ if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
+ }
+
PIDE.spell_checker.update(PIDE.options.value)
PIDE.session.update_options(PIDE.options.value)