# HG changeset patch
# User wenzelm
# Date 1497040128 -7200
# Node ID cf35abfb9ebc9c0d2979a1bd1d0df05640aadffe
# Parent  07175635f78c2ed0880e8f9cf885e4010941acdd
clarified output for symbol completion;

diff -r 07175635f78c -r cf35abfb9ebc src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Fri Jun 09 21:57:30 2017 +0200
+++ b/src/Pure/General/completion.scala	Fri Jun 09 22:28:48 2017 +0200
@@ -415,7 +415,6 @@
     caret: Int,
     language_context: Completion.Language_Context): Option[Completion.Result] =
   {
-    def decode(s: String): String = if (unicode) Symbol.decode(s) else s
     val length = text.length
 
     val abbrevs_result =
@@ -477,17 +476,21 @@
               Character.codePointCount(original, 0, original.length) > 1)
         val unique = completions.length == 1
 
+        def decode1(s: String): String = if (unicode) Symbol.decode(s) else s
+        def decode2(s: String): String = if (unicode) s else Symbol.decode(s)
+
         val items =
           for {
             (complete_word, name0) <- completions
-            name1 = decode(name0)
+            name1 = decode1(name0)
+            name2 = decode2(name0)
             if name1 != original
             (s1, s2) = Completion.split_template(name1)
             move = - s2.length
             description =
               if (is_symbol(name0)) {
-                if (name0 == name1) List(name0)
-                else List(name1, "(symbol " + quote(name0) + ")")
+                if (name1 == name2) List(name1)
+                else List(name1, "(symbol " + quote(name2) + ")")
               }
               else if (is_keyword_template(complete_word, true))
                 List(name1, "(template " + quote(complete_word) + ")")