# HG changeset patch
# User wenzelm
# Date 1728244531 -7200
# Node ID c531629c391a3dc80dffca655b8fe769bad8bfe2
# Parent  84e459f091984f5c28ecc411868acfe0870f8239
tuned output;

diff -r 84e459f09198 -r c531629c391a 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), _))) =>