src/Tools/jEdit/src/plugin.scala
changeset 65242 63a64779d586
parent 65241 6f00727f0d41
child 65243 ba5ce07e06a7
equal deleted inserted replaced
65241:6f00727f0d41 65242:63a64779d586
   372             val buffer = edit_pane.getBuffer
   372             val buffer = edit_pane.getBuffer
   373             val text_area = edit_pane.getTextArea
   373             val text_area = edit_pane.getTextArea
   374             if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
   374             if (buffer != null && text_area != null) PIDE.init_view(buffer, text_area)
   375           }
   375           }
   376 
   376 
   377           PIDE.plugin.spell_checker.update(PIDE.options.value)
   377           spell_checker.update(PIDE.options.value)
   378           PIDE.session.update_options(PIDE.options.value)
   378           PIDE.session.update_options(PIDE.options.value)
   379 
   379 
   380         case _ =>
   380         case _ =>
   381       }
   381       }
   382     }
   382     }
   385   override def start()
   385   override def start()
   386   {
   386   {
   387     try {
   387     try {
   388       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   388       Debug.DISABLE_SEARCH_DIALOG_POOL = true
   389 
   389 
   390       PIDE.plugin.completion_history.load()
   390       completion_history.load()
   391       PIDE.plugin.spell_checker.update(PIDE.options.value)
   391       spell_checker.update(PIDE.options.value)
   392 
   392 
   393       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   393       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
   394       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   394       if (ModeProvider.instance.isInstanceOf[ModeProvider])
   395         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   395         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
   396 
   396 
   420   {
   420   {
   421     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   421     JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _)
   422 
   422 
   423     if (startup_failure.isEmpty) {
   423     if (startup_failure.isEmpty) {
   424       PIDE.options.value.save_prefs()
   424       PIDE.options.value.save_prefs()
   425       PIDE.plugin.completion_history.value.save()
   425       completion_history.value.save()
   426     }
   426     }
   427 
   427 
   428     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   428     PIDE.exit_models(JEdit_Lib.jedit_buffers().toList)
   429     PIDE.session.stop()
   429     PIDE.session.stop()
   430     PIDE.file_watcher.shutdown()
   430     PIDE.file_watcher.shutdown()