changeset 59319 | 677615cba30d |
parent 59073 | dcecfcc56dce |
child 59717 | 44a3ed0b8265 |
--- a/src/Pure/General/completion.scala Wed Jan 07 18:09:11 2015 +0100 +++ b/src/Pure/General/completion.scala Thu Jan 08 20:56:39 2015 +0100 @@ -416,7 +416,7 @@ } (abbrevs_result orElse words_result) match { - case Some((original, completions)) if !completions.isEmpty => + case Some((original, completions)) if completions.nonEmpty => val range = Text.Range(- original.length, 0) + caret + start val immediate = explicit ||