diff -r e4152e64698f -r 36c5eabd62ec src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Thu Dec 26 12:03:56 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Thu Dec 26 12:08:05 2024 +0100
@@ -160,6 +160,10 @@
 
   /* tooltips */
 
+  def gui_name(name: String, kind: String = "", prefix: String = ""): String =
+    GUI.Name(name, kind = Word.informal(kind), prefix = prefix,
+      style = GUI.Style.symbol_decoded).toString
+
   def get_tooltip_description(name: String): Option[String] = tooltip_description.get(name)
 
   private val tooltip_description =
@@ -670,30 +674,25 @@
 
           case (info, Text.Info(r0, XML.Elem(Markup.Entity(kind, name), _)))
           if kind != "" && kind != Markup.ML_DEF =>
-            val kind1 = Word.informal(kind)
-            val txt1 =
-              if (name == "") kind1
-              else if (kind1 == "") quote(name)
-              else kind1 + " " + quote(name)
-            val info1 = info.add_info_text(r0, txt1, ord = 2)
+            val txt = Rendering.gui_name(name, kind = kind)
+            val info1 = info.add_info_text(r0, txt, ord = 2)
             Some(if (kind == Markup.COMMAND) info1.add_info(r0, XML.elem(Markup.TIMING)) else info1)
 
           case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
             val file = perhaps_append_file(snapshot.node_name, name)
             val info1 =
               if (name == file) info
-              else info.add_info_text(r0, "path " + quote(name))
-            Some(info1.add_info_text(r0, "file " + quote(file)))
+              else info.add_info_text(r0, Rendering.gui_name(name, kind = "path"))
+            Some(info1.add_info_text(r0, Rendering.gui_name(file, kind = "file")))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Doc(name), _))) =>
-            val text = "doc " + quote(name)
-            Some(info.add_info_text(r0, text))
+            Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "doc")))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Url(name), _))) =>
-            Some(info.add_info_text(r0, "URL " + quote(name)))
+            Some(info.add_info_text(r0, Rendering.gui_name(name, kind = "URL")))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Command_Span(span), _))) =>
-            Some(info.add_info_text(r0, "command span " + quote(span.name)))
+            Some(info.add_info_text(r0, Rendering.gui_name(span.name, kind = Markup.COMMAND_SPAN)))
 
           case (info, Text.Info(r0, XML.Elem(Markup(name, _), body)))
           if name == Markup.SORTING || name == Markup.TYPING =>
@@ -716,12 +715,12 @@
             Some(info.add_info_text(r0, "language: " + lang.description))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
-            val descr = GUI.Name(name, kind = Word.informal(kind), prefix = Markup.NOTATION)
-            Some(info.add_info_text(r0, descr.toString, ord = 1))
+            val description = Rendering.gui_name(name, kind = kind, prefix = Markup.NOTATION)
+            Some(info.add_info_text(r0, description, ord = 1))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind, name), _))) =>
-            val descr = GUI.Name(name, kind = Word.informal(kind), prefix = Markup.EXPRESSION)
-            Some(info.add_info_text(r0, descr.toString, ord = 1))
+            val description = Rendering.gui_name(name, kind = kind, prefix = Markup.EXPRESSION)
+            Some(info.add_info_text(r0, description, ord = 1))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(info.add_info_text(r0, "Markdown: paragraph"))