tuned signature;
authorwenzelm
Thu, 15 Jul 2021 21:11:39 +0200
changeset 73997 0f61cd0ce803
parent 73996 f3409ced4df2
child 73998 b3f2da6bef51
tuned signature;
src/Tools/jEdit/src/main_plugin.scala
src/Tools/jEdit/src/syntax_style.scala
--- a/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:21:16 2021 +0200
+++ b/src/Tools/jEdit/src/main_plugin.scala	Thu Jul 15 21:11:39 2021 +0200
@@ -454,7 +454,7 @@
 
       JEdit_Lib.jedit_views().foreach(init_title)
 
-      Syntax_Style.set_extender(Syntax_Style.Extender)
+      Syntax_Style.set_extender(Syntax_Style.Main_Extender)
       init_mode_provider()
       JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
 
--- a/src/Tools/jEdit/src/syntax_style.scala	Thu Jul 15 21:21:16 2021 +0200
+++ b/src/Tools/jEdit/src/syntax_style.scala	Thu Jul 15 21:11:39 2021 +0200
@@ -81,7 +81,7 @@
     }
   }
 
-  object Extender extends SyntaxUtilities.StyleExtender
+  object Main_Extender extends SyntaxUtilities.StyleExtender
   {
     val max_user_fonts = 2
     if (Symbol.font_names.length > max_user_fonts)