# HG changeset patch
# User wenzelm
# Date 1447190868 -3600
# Node ID 8bb7848b3d4749751f5d1f3acbeb9e5f0f428b9f
# Parent  70b8085f51b4bf5be6d6132575f100e84439440e
smart quoting of non-identifiers, e.g. jEdit actions;

diff -r 70b8085f51b4 -r 8bb7848b3d47 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)))