--- a/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 20:44:48 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_spell_checker.scala Mon Jun 19 21:09:19 2017 +0200
@@ -21,14 +21,14 @@
{
/* completion */
- def completion(rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset)
- : Option[Completion.Result] =
+ def completion(
+ rendering: JEdit_Rendering, explicit: Boolean, caret: Text.Offset): Option[Completion.Result] =
{
- for {
- spell_checker <- PIDE.plugin.spell_checker.get
- if explicit
- res <- spell_checker.completion(rendering, caret)
- } yield res
+ PIDE.plugin.spell_checker.get match {
+ case Some(spell_checker) if explicit =>
+ spell_checker.completion(rendering, caret)
+ case _ => None
+ }
}