src/Pure/General/completion.scala
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 ||