# HG changeset patch
# User wenzelm
# Date 1734959383 -3600
# Node ID ae670d8609125400fe20662958a483e70e2f1c0b
# Parent  4c51d3341de8d1b350778ce42f1d032b6062b8a7
tuned signature;

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 =
diff -r 4c51d3341de8 -r ae670d860912 src/Pure/General/word.scala
--- a/src/Pure/General/word.scala	Sun Dec 22 14:21:39 2024 +0100
+++ b/src/Pure/General/word.scala	Mon Dec 23 14:09:43 2024 +0100
@@ -76,6 +76,8 @@
   def explode(text: String): List[String] =
     explode(Character.isWhitespace _, text)
 
+  def informal(text: String): String = implode(explode('_', text))
+
 
   /* brackets */
 
diff -r 4c51d3341de8 -r ae670d860912 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sun Dec 22 14:21:39 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Mon Dec 23 14:09:43 2024 +0100
@@ -238,7 +238,7 @@
     def is_antiquotation: Boolean = name == Language.ANTIQUOTATION
     def is_path: Boolean = name == Language.PATH
 
-    def description: String = Word.implode(Word.explode('_', name))
+    def description: String = Word.informal(name)
   }
 
 
diff -r 4c51d3341de8 -r ae670d860912 src/Pure/PIDE/rendering.scala
--- 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)