smart quoting of non-identifiers, e.g. jEdit actions;
authorwenzelm
Tue, 10 Nov 2015 22:27:48 +0100
changeset 61622 8bb7848b3d47
parent 61621 70b8085f51b4
child 61623 2f89f0b13e08
smart quoting of non-identifiers, e.g. jEdit actions;
src/Pure/General/completion.scala
--- a/src/Pure/General/completion.scala	Tue Nov 10 22:20:46 2015 +0100
+++ b/src/Pure/General/completion.scala	Tue Nov 10 22:27:48 2015 +0100
@@ -205,8 +205,15 @@
              (Long_Name.qualify(kind, name),
               Word.implode(Word.explode('_', kind)) +
               (if (xname == name) "" else " " + quote(decode(name))))
-          description = List(xname1, "(" + descr_name + ")")
-        } yield Item(range, original, full_name, description, xname1, 0, true)
+        } yield {
+          val description = List(xname1, "(" + descr_name + ")")
+          val replacement =
+            Token.explode(Keyword.Keywords.empty, xname1) match {
+              case List(tok) if tok.is_name => xname1
+              case _ => quote(xname1)
+            }
+          Item(range, original, full_name, description, replacement, 0, true)
+        }
 
       if (items.isEmpty) None
       else Some(Result(range, original, names.length == 1, items.sorted(history.ordering)))