equal
deleted
inserted
replaced
445 } |
445 } |
446 } |
446 } |
447 |
447 |
448 override def stop() |
448 override def stop() |
449 { |
449 { |
450 SyntaxUtilities.setStyleExtender(Syntax_Style.No_Extender) |
|
451 exit_mode_provider() |
450 exit_mode_provider() |
452 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) |
451 JEdit_Lib.jedit_text_areas.foreach(Completion_Popup.Text_Area.exit _) |
453 |
452 |
454 if (startup_failure.isEmpty) { |
453 if (startup_failure.isEmpty) { |
455 options.value.save_prefs() |
454 options.value.save_prefs() |