author | wenzelm |
Wed, 13 Apr 2016 11:26:52 +0200 | |
changeset 62964 | d0c1b2dbca5b |
parent 62962 | 1c1f8531ca37 |
child 62965 | 5bf08c9aa036 |
--- 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)