# HG changeset patch
# User wenzelm
# Date 1489523073 -3600
# Node ID 63a64779d586b7675f006c8943e41dfb10fa4638
# Parent  6f00727f0d419fbc63e2f9742c4b5b209c05f1e8
tuned;

diff -r 6f00727f0d41 -r 63a64779d586 src/Tools/jEdit/src/plugin.scala
--- 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)