# HG changeset patch
# User wenzelm
# Date 1460539612 -7200
# Node ID d0c1b2dbca5b76baacaa2492b2ad792e09bbbc8e
# Parent  1c1f8531ca372e8efd14d6b188004bbe35e6e48d
avoid quotes for qualified names;

diff -r 1c1f8531ca37 -r d0c1b2dbca5b src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Apr 12 18:49:39 2016 +0200
+++ b/src/Pure/General/completion.scala	Wed Apr 13 11:26:52 2016 +0200
@@ -209,7 +209,7 @@
           val description = List(xname1, "(" + descr_name + ")")
           val replacement =
             Token.explode(Keyword.Keywords.empty, xname1) match {
-              case List(tok) if tok.is_name => xname1
+              case List(tok) if tok.is_xname => xname1
               case _ => quote(xname1)
             }
           Item(range, original, full_name, description, replacement, 0, true)