--- a/src/Tools/jEdit/src/jedit_lib.scala Thu Feb 04 21:28:56 2016 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala Thu Feb 04 21:53:06 2016 +0100
@@ -16,7 +16,7 @@
import scala.annotation.tailrec
import scala.util.parsing.input.CharSequenceReader
-import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug}
+import org.gjt.sp.jedit.{jEdit, Buffer, View, GUIUtilities, Debug, EditPane}
import org.gjt.sp.jedit.gui.KeyEventWorkaround
import org.gjt.sp.jedit.buffer.{JEditBuffer, LineManager}
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
@@ -130,6 +130,10 @@
def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+ def jedit_edit_panes(view: View): Iterator[EditPane] =
+ if (view == null) Iterator.empty
+ else view.getEditPanes().iterator.filter(_ != null)
+
def jedit_text_areas(view: View): Iterator[JEditTextArea] =
if (view == null) Iterator.empty
else view.getEditPanes().iterator.filter(_ != null).map(_.getTextArea).filter(_ != null)
--- 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)