# HG changeset patch
# User wenzelm
# Date 1504531525 -7200
# Node ID 180b2e72601fc5524b718e68364a1a2f3942bb51
# Parent  af3cf2c859c1fc9ae7b21bcca3e1f4627d47c4a0
more thorough change of syntax style extender: jEdit.propertiesChanged invalidates buffer chunk cache;

diff -r af3cf2c859c1 -r 180b2e72601f src/Tools/jEdit/src-base/plugin.scala
--- a/src/Tools/jEdit/src-base/plugin.scala	Sun Sep 03 16:35:34 2017 +0200
+++ b/src/Tools/jEdit/src-base/plugin.scala	Mon Sep 04 15:25:25 2017 +0200
@@ -21,11 +21,11 @@
 
     Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
-    SyntaxUtilities.setStyleExtender(Syntax_Style.Dummy_Extender)
+    Syntax_Style.dummy_style_extender()
   }
 
   override def stop()
   {
-    SyntaxUtilities.setStyleExtender(new SyntaxUtilities.StyleExtender)
+    Syntax_Style.set_style_extender(new SyntaxUtilities.StyleExtender)
   }
 }
diff -r af3cf2c859c1 -r 180b2e72601f src/Tools/jEdit/src-base/syntax_style.scala
--- a/src/Tools/jEdit/src-base/syntax_style.scala	Sun Sep 03 16:35:34 2017 +0200
+++ b/src/Tools/jEdit/src-base/syntax_style.scala	Mon Sep 04 15:25:25 2017 +0200
@@ -11,6 +11,7 @@
 
 import org.gjt.sp.util.SyntaxUtilities
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, SyntaxStyle}
+import org.gjt.sp.jedit.jEdit
 
 
 object Syntax_Style
@@ -29,4 +30,12 @@
       new_styles
     }
   }
+
+  def set_style_extender(extender: SyntaxUtilities.StyleExtender)
+  {
+    SyntaxUtilities.setStyleExtender(extender)
+    GUI_Thread.later { jEdit.propertiesChanged }
+  }
+
+  def dummy_style_extender() { set_style_extender(Dummy_Extender) }
 }
diff -r af3cf2c859c1 -r 180b2e72601f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sun Sep 03 16:35:34 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 04 15:25:25 2017 +0200
@@ -316,6 +316,8 @@
               GUI.scrollable_text(cat_lines(resources.session_errors)))
           }
 
+          jEdit.propertiesChanged()
+
           val view = jEdit.getActiveView()
           init_view(view)
 
@@ -428,7 +430,7 @@
       completion_history.load()
       spell_checker.update(options.value)
 
-      SyntaxUtilities.setStyleExtender(Syntax_Style.Extender)
+      isabelle.jedit_base.Syntax_Style.set_style_extender(Syntax_Style.Extender)
       init_mode_provider()
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
@@ -451,7 +453,7 @@
   {
     http_server.stop
 
-    SyntaxUtilities.setStyleExtender(isabelle.jedit_base.Syntax_Style.Dummy_Extender)
+    isabelle.jedit_base.Syntax_Style.dummy_style_extender()
     exit_mode_provider()
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)