keep style extender for the sake of potentially remaining token markers;

--- a/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 15:50:28 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Mar 15 16:55:37 2017 +0100
@@ -447,7 +447,6 @@
 
   override def stop()
   {
-    SyntaxUtilities.setStyleExtender(Syntax_Style.No_Extender)
     exit_mode_provider()
     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
 

--- a/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 15:50:28 2017 +0100
+++ b/src/Tools/jEdit/src/syntax_style.scala	Wed Mar 15 16:55:37 2017 +0100
@@ -60,8 +60,6 @@
 
   val hidden_color: Color = new Color(255, 255, 255, 0)
 
-  object No_Extender extends SyntaxUtilities.StyleExtender
-
   object Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2