src/Tools/jEdit/src/plugin.scala
changeset 65242 63a64779d586
parent 65241 6f00727f0d41
child 65243 ba5ce07e06a7
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:14:57 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 14 21:24:33 2017 +0100
@@ -374,7 +374,7 @@
             if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
           }
 
-          PIDE.plugin.spell_checker.update(PIDE.options.value)
+          spell_checker.update(PIDE.options.value)
           PIDE.session.update_options(PIDE.options.value)
 
         case _ =>
@@ -387,8 +387,8 @@
     try {
       Debug.DISABLE_SEARCH_DIALOG_POOL = true
 
-      PIDE.plugin.completion_history.load()
-      PIDE.plugin.spell_checker.update(PIDE.options.value)
+      completion_history.load()
+      spell_checker.update(PIDE.options.value)
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
@@ -422,7 +422,7 @@
 
     if (startup_failure.isEmpty) {
       PIDE.options.value.save_prefs()
-      PIDE.plugin.completion_history.value.save()
+      completion_history.value.save()
     }
 
     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)