src/Tools/jEdit/src/completion_popup.scala
changeset 57051 5e30ffe79980
parent 56877 4e9d2eab9cfa
child 57127 a406e15c3cf7
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed May 21 20:36:22 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed May 21 22:06:10 2014 +0200
     1.3 @@ -181,10 +181,13 @@
     1.4  
     1.5      /* spell-checker completion */
     1.6  
     1.7 -    def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
     1.8 +    def spell_checker_completion(
     1.9 +      explicit: Boolean,
    1.10 +      rendering: Rendering): Option[Completion.Result] =
    1.11      {
    1.12        for {
    1.13          spell_checker <- PIDE.spell_checker.get
    1.14 +        if explicit
    1.15          range = JEdit_Lib.before_caret_range(text_area, rendering)
    1.16          word <- Spell_Checker.current_word(text_area, rendering, range)
    1.17          words = spell_checker.complete(word.info)
    1.18 @@ -395,7 +398,7 @@
    1.19                case Some(rendering) =>
    1.20                  Completion.Result.merge(history, result0,
    1.21                    Completion.Result.merge(history,
    1.22 -                    spell_checker_completion(rendering), path_completion(rendering)))
    1.23 +                    spell_checker_completion(explicit, rendering), path_completion(rendering)))
    1.24              }
    1.25            }
    1.26            result match {