diff -r 4c51d3341de8 -r ae670d860912 src/Pure/General/completion.scala --- a/src/Pure/General/completion.scala Sun Dec 22 14:21:39 2024 +0100 +++ b/src/Pure/General/completion.scala Mon Dec 23 14:09:43 2024 +0100 @@ -198,8 +198,7 @@ if (kind == "") (name, quote(decode(name))) else (Long_Name.qualify(kind, name), - Word.implode(Word.explode('_', kind)) + - (if (xname == name) "" else " " + quote(decode(name)))) + Word.informal(kind) + (if (xname == name) "" else " " + quote(decode(name)))) } yield { val description = List(xname1, "(" + descr_name + ")") val replacement =