# HG changeset patch
# User wenzelm
# Date 1497899359 -7200
# Node ID 0b257d7d81a5e96f0f55f4327ce5ffcb746a5485
# Parent  03dd799fe0423d20a555252dc06aa608ea50110c
tuned;

diff -r 03dd799fe042 -r 0b257d7d81a5 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
+    }
   }