# HG changeset patch
# User wenzelm
# Date 1735048796 -3600
# Node ID c98cfdcb2df035fc899719ffb9881bec0e49e261
# Parent  ae670d8609125400fe20662958a483e70e2f1c0b
clarified signature;

diff -r ae670d860912 -r c98cfdcb2df0 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Mon Dec 23 14:09:43 2024 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 24 14:59:56 2024 +0100
@@ -67,6 +67,18 @@
   }
 
 
+  /* named items */
+
+  sealed case class Name(name: String, kind: String = "", prefix: String = "") {
+    override def toString: String = {
+      val a = kind.nonEmpty
+      val b = name.nonEmpty
+      prefix + if_proper(a || b,
+        if_proper(prefix, ": ") + kind + if_proper(a && b, " ") + if_proper(b, quote(name)))
+    }
+  }
+
+
   /* simple dialogs */
 
   def scrollable_text(
diff -r ae670d860912 -r c98cfdcb2df0 src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Mon Dec 23 14:09:43 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Tue Dec 24 14:59:56 2024 +0100
@@ -172,14 +172,6 @@
       Markup.TFREE -> "free type variable",
       Markup.TVAR -> "schematic type variable")
 
-  def tooltip_text(markup: String, kind: String, name: String): String = {
-    val a = kind.nonEmpty
-    val b = name.nonEmpty
-    val k = Word.informal(kind)
-    if (!a && !b) markup
-    else markup + ": " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
-  }
-
 
   /* entity focus */
 
@@ -724,12 +716,12 @@
             Some(info.add_info_text(r0, "language: " + lang.description))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
-            val description = Rendering.tooltip_text(Markup.NOTATION, kind, name)
-            Some(info.add_info_text(r0, description, ord = 1))
+            val descr = GUI.Name(name, kind = Word.informal(kind), prefix = Markup.NOTATION)
+            Some(info.add_info_text(r0, descr.toString, ord = 1))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind, name), _))) =>
-            val description = Rendering.tooltip_text(Markup.EXPRESSION, kind, name)
-            Some(info.add_info_text(r0, description, ord = 1))
+            val descr = GUI.Name(name, kind = Word.informal(kind), prefix = Markup.EXPRESSION)
+            Some(info.add_info_text(r0, descr.toString, ord = 1))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(info.add_info_text(r0, "Markdown: paragraph"))