tuned;
authorwenzelm
Mon, 19 Jun 2017 21:09:19 +0200
changeset 66119 0b257d7d81a5
parent 66118 03dd799fe042
child 66120 e03ff7e831cc
tuned;
src/Tools/jEdit/src/jedit_spell_checker.scala
--- 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
+    }
   }