src/Tools/jEdit/src/plugin.scala
changeset 66602 180b2e72601f
parent 66593 d389714a8aaa
child 66714 9fc4e144693c
--- 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 _)