# HG changeset patch
# User wenzelm
# Date 1400702770 -7200
# Node ID 5e30ffe79980867dfae24d83c35930118a0339f2
# Parent  362c8c64ec8327fef506a97548d1099d11d13506
spell-checker completion is restricted to explicit mode, to avoid odd effects with immediate edits vs. delayed language context markup, and occasional delays due to dictionary lookup of many variants;

diff -r 362c8c64ec83 -r 5e30ffe79980 src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed May 21 20:36:22 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed May 21 22:06:10 2014 +0200
@@ -181,10 +181,13 @@
 
     /* spell-checker completion */
 
-    def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
+    def spell_checker_completion(
+      explicit: Boolean,
+      rendering: Rendering): Option[Completion.Result] =
     {
       for {
         spell_checker <- PIDE.spell_checker.get
+        if explicit
         range = JEdit_Lib.before_caret_range(text_area, rendering)
         word <- Spell_Checker.current_word(text_area, rendering, range)
         words = spell_checker.complete(word.info)
@@ -395,7 +398,7 @@
               case Some(rendering) =>
                 Completion.Result.merge(history, result0,
                   Completion.Result.merge(history,
-                    spell_checker_completion(rendering), path_completion(rendering)))
+                    spell_checker_completion(explicit, rendering), path_completion(rendering)))
             }
           }
           result match {