# HG changeset patch
# User wenzelm
# Date 1734534187 -3600
# Node ID 5b87f8dacd8e9854a92b5ac219fc282d913656d8
# Parent  79079d94095b392820584f0ef933904a3be8bb6c
more uniform Markup.notation vs. Markup.expression;

diff -r 79079d94095b -r 5b87f8dacd8e src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Wed Dec 18 14:53:31 2024 +0100
+++ b/src/Pure/PIDE/markup.scala	Wed Dec 18 16:03:07 2024 +0100
@@ -179,9 +179,9 @@
 
   val EXPRESSION = "expression"
   object Expression {
-    def unapply(markup: Markup): Option[String] =
+    def unapply(markup: Markup): Option[(String, String)] =
       markup match {
-        case Markup(EXPRESSION, props) => Some(Kind.get(props))
+        case Markup(EXPRESSION, props) => Some((Kind.get(props), Name.get(props)))
         case _ => None
       }
 
diff -r 79079d94095b -r 5b87f8dacd8e src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Wed Dec 18 14:53:31 2024 +0100
+++ b/src/Pure/PIDE/rendering.scala	Wed Dec 18 16:03:07 2024 +0100
@@ -172,6 +172,14 @@
       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.implode(Word.explode('_', kind))
+    if (!a && !b) markup
+    else markup + ": " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
+  }
+
 
   /* entity focus */
 
@@ -716,18 +724,11 @@
             Some(info.add_info_text(r0, "language: " + lang.description))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Notation(kind, name), _))) =>
-            val a = kind.nonEmpty
-            val b = name.nonEmpty
-            val k = Word.implode(Word.explode('_', kind))
-            val description =
-              if (!a && !b) "notation"
-              else "notation: " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
+            val description = Rendering.tooltip_text(Markup.NOTATION, kind, name)
             Some(info.add_info_text(r0, description, ord = 1))
 
-          case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>
-            val description =
-              if (kind.isEmpty) "expression"
-              else "expression: " + Word.implode(Word.explode('_', kind))
+          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))
 
           case (info, Text.Info(r0, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>