# HG changeset patch
# User wenzelm
# Date 1394220254 -3600
# Node ID 594afef0dd89e32ae74a3268018a0b82c5463712
# Parent  2aaecd737d753811bf9fb11274e90ff939e5b2fb
tuned;

diff -r 2aaecd737d75 -r 594afef0dd89 src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Mar 07 20:12:38 2014 +0100
+++ b/src/Pure/General/completion.scala	Fri Mar 07 20:24:14 2014 +0100
@@ -265,8 +265,8 @@
 {
   /* keywords */
 
-  def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
-  def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
+  private def is_keyword(name: String): Boolean = keywords.isDefinedAt(name)
+  private def is_keyword_template(name: String): Boolean = keywords.get(name) == Some(true)
 
   def + (keyword: String, template: String): Completion =
     new Completion(
@@ -281,6 +281,9 @@
 
   /* symbols with abbreviations */
 
+  private def is_symbol(name: String): Boolean =
+    Symbol.names.isDefinedAt(name)
+
   private def add_symbols(): Completion =
   {
     val words =
@@ -369,38 +372,40 @@
     (abbrevs_result orElse words_result) match {
       case Some(((original, completions0), end)) =>
         val completions1 = completions0.map(decode(_))
-        if (completions1.exists(_ != original)) {
-          val range = Text.Range(- original.length, 0) + end + start
-          val immediate =
-            explicit ||
-              (!Completion.Word_Parsers.is_word(original) &&
-                Character.codePointCount(original, 0, original.length) > 1)
-          val unique = completions0.length == 1
-          val items =
-            for {
-              (name0, name1) <- completions0 zip completions1
-              if name1 != original
-              (s1, s2) =
-                space_explode(Completion.caret_indicator, name1) match {
-                  case List(s1, s2) => (s1, s2)
-                  case _ => (name1, "")
-                }
-              move = - s2.length
-              description =
-                if (Symbol.names.isDefinedAt(name0)) {
-                  if (name0 == name1) List(name0)
-                  else List(name1, "(symbol " + quote(name0) + ")")
-                }
-                else if (move != 0 || is_keyword_template(name0))
-                  List(name1, "(template)")
-                else if (is_keyword(name0))
-                  List(name1, "(keyword)")
-                else List(name1)
-            }
-            yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
-          Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
-        }
-        else None
+
+        val range = Text.Range(- original.length, 0) + end + start
+        val immediate =
+          explicit ||
+            (!Completion.Word_Parsers.is_word(original) &&
+              Character.codePointCount(original, 0, original.length) > 1)
+        val unique = completions0.length == 1
+
+        val items =
+          for {
+            (name0, name1) <- completions0 zip completions1
+            if name1 != original
+            (s1, s2) =
+              space_explode(Completion.caret_indicator, name1) match {
+                case List(s1, s2) => (s1, s2)
+                case _ => (name1, "")
+              }
+            move = - s2.length
+            description =
+              if (is_symbol(name0)) {
+                if (name0 == name1) List(name0)
+                else List(name1, "(symbol " + quote(name0) + ")")
+              }
+              else if (move != 0 || is_keyword_template(name0))
+                List(name1, "(template)")
+              else if (is_keyword(name0))
+                List(name1, "(keyword)")
+              else List(name1)
+          }
+          yield Completion.Item(range, original, name1, description, s1 + s2, move, immediate)
+
+        if (items.isEmpty) None
+        else Some(Completion.Result(range, original, unique, items.sorted(history.ordering)))
+
       case None => None
     }
   }