# HG changeset patch
# User wenzelm
# Date 1489593337 -3600
# Node ID f994a61376eb814ed620010718ae337613948578
# Parent  7e6ecd04b5fe202ef289567e5b5b9ccb6fed157c
keep style extender for the sake of potentially remaining token markers;

diff -r 7e6ecd04b5fe -r f994a61376eb src/Tools/jEdit/src/plugin.scala
--- 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 _)
 
diff -r 7e6ecd04b5fe -r f994a61376eb src/Tools/jEdit/src/syntax_style.scala
--- 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