--- a/src/Tools/jEdit/src/plugin.scala Wed Mar 15 13:49:39 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala Wed Mar 15 14:04:58 2017 +0100
@@ -356,6 +356,30 @@
}
}
+
+ /* mode provider */
+
+ private var orig_mode_provider: ModeProvider = null
+ private var pide_mode_provider: ModeProvider = null
+
+ def init_mode_provider()
+ {
+ orig_mode_provider = ModeProvider.instance
+ if (orig_mode_provider.isInstanceOf[ModeProvider]) {
+ pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
+ ModeProvider.instance = pide_mode_provider
+ }
+ }
+
+ def exit_mode_provider()
+ {
+ if (ModeProvider.instance == pide_mode_provider)
+ ModeProvider.instance = orig_mode_provider
+ }
+
+
+ /* start and stop */
+
override def start()
{
/* strict initialization */
@@ -382,9 +406,7 @@
spell_checker.update(options.value)
SyntaxUtilities.setStyleExtender(new Syntax_Style.Extender)
- if (ModeProvider.instance.isInstanceOf[ModeProvider])
- ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
-
+ init_mode_provider()
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.init _)
val resources = new JEdit_Resources(JEdit_Sessions.session_base(options.value))
@@ -410,6 +432,7 @@
override def stop()
{
JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
+ exit_mode_provider()
if (startup_failure.isEmpty) {
options.value.save_prefs()