# HG changeset patch # User wenzelm # Date 1472754883 -7200 # Node ID 2ca536d0163eb042ddb016e83050523f3538097c # Parent b1088b1e3b7e69531b25bc872903e5ec5d2adabb more careful quoting, e.g. relevant for \<^control>cartouche; diff -r b1088b1e3b7e -r 2ca536d0163e src/Pure/General/completion.scala --- 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)