# HG changeset patch
# User wenzelm
# Date 1454619186 -3600
# Node ID 340f98836fd9503527d85ec984f4249bcb0fd0ff
# Parent  2c76c66897fca72e0c1de06b7e586acd5faa3a15
re-init document views for the sake of Text_Overview size;

diff -r 2c76c66897fc -r 340f98836fd9 src/Tools/jEdit/src/jedit_lib.scala
--- 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)
diff -r 2c76c66897fc -r 340f98836fd9 src/Tools/jEdit/src/plugin.scala
--- 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)