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