# HG changeset patch
# User wenzelm
# Date 1489583316 -3600
# Node ID 034c49653a8e473d88674d119d672a35ec05b906
# Parent  ff9cc2f38dd31d669878b1d5d94614440e6ea6ef
clarified initialization;
tuned;

diff -r ff9cc2f38dd3 -r 034c49653a8e src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 14:04:58 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 14:08:36 2017 +0100
@@ -405,7 +405,7 @@
       completion_history.load()
       spell_checker.update(options.value)
 
-      SyntaxUtilities.setStyleExtender(new Syntax_Style.Extender)
+      SyntaxUtilities.setStyleExtender(Syntax_Style.Extender)
       init_mode_provider()
       JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
 
@@ -431,8 +431,9 @@
 
   override def stop()
   {
+    SyntaxUtilities.setStyleExtender(Syntax_Style.No_Extender)
+    exit_mode_provider()
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
-    exit_mode_provider()
 
     if (startup_failure.isEmpty) {
       options.value.save_prefs()
diff -r ff9cc2f38dd3 -r 034c49653a8e src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 14:04:58 2017 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 14:08:36 2017 +0100
@@ -60,7 +60,9 @@
 
   val hidden_color: Color = new Color(255, 255, 255, 0)
 
-  class Extender extends SyntaxUtilities.StyleExtender
+  object No_Extender extends SyntaxUtilities.StyleExtender
+
+  object Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2
     if (Symbol.font_names.length > max_user_fonts)