--- a/src/Pure/PIDE/rendering.scala Sun Dec 22 14:21:39 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala Mon Dec 23 14:09:43 2024 +0100
@@ -175,7 +175,7 @@
def tooltip_text(markup: String, kind: String, name: String): String = {
val a = kind.nonEmpty
val b = name.nonEmpty
- val k = Word.implode(Word.explode('_', kind))
+ val k = Word.informal(kind)
if (!a && !b) markup
else markup + ": " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
}
@@ -678,7 +678,7 @@
case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
if kind != "" && kind != Markup.ML_DEF =>
- val kind1 = Word.implode(Word.explode('_', kind))
+ val kind1 = Word.informal(kind)
val txt1 =
if (name == "") kind1
else if (kind1 == "") quote(name)