src/Pure/General/completion.scala
changeset 81647 ae670d860912
parent 77368 7c57d9586f4c
--- 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 =