diff -r d59cc10a6888 -r 7ea69c26524b src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Thu Jul 04 19:16:12 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Fri Jul 05 00:12:32 2024 +0200
@@ -102,7 +102,7 @@
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
-  else (XY ^ name ^ implode (map (fn (a, x) => Y ^ a ^ "=" ^ x) atts) ^ X, XYX);
+  else (XY ^ name ^ implode (map (fn p => Y ^ Properties.print_eq p) atts) ^ X, XYX);
 
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))