tuned output;
authorwenzelm
Sun, 06 Oct 2024 21:55:31 +0200
changeset 81123 c531629c391a
parent 81122 84e459f09198
child 81124 6ce0c8d59f5a
tuned output;
src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Sun Oct 06 21:54:53 2024 +0200
+++ b/src/Pure/PIDE/rendering.scala	Sun Oct 06 21:55:31 2024 +0200
@@ -670,9 +670,10 @@
           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: " + kind + if_proper(a && b, " ") + if_proper(b, quote(name))
+              else "notation: " + k + if_proper(a && b, " ") + if_proper(b, quote(name))
             Some(info + (r0, true, XML.Text(description)))
 
           case (info, Text.Info(r0, XML.Elem(Markup.Expression(kind), _))) =>