src/Pure/General/completion.scala
changeset 63761 2ca536d0163e
parent 63587 881e8e2cfec2
child 63808 e8462a4349fc
--- a/src/Pure/General/completion.scala	Thu Sep 01 20:14:29 2016 +0200
+++ b/src/Pure/General/completion.scala	Thu Sep 01 20:34:43 2016 +0200
@@ -208,8 +208,10 @@
         } yield {
           val description = List(xname1, "(" + descr_name + ")")
           val replacement =
-            Token.explode(Keyword.Keywords.empty, xname1) match {
-              case List(tok) if tok.is_name => xname1
+            List(original, xname1).map(Token.explode(Keyword.Keywords.empty, _)) match {
+              case List(List(tok), _) if tok.kind == Token.Kind.CARTOUCHE =>
+                Symbol.open_decoded + xname1 + Symbol.close_decoded
+              case List(_, List(tok)) if tok.is_name => xname1
               case _ => quote(xname1)
             }
           Item(range, original, full_name, description, replacement, 0, true)