# HG changeset patch
# User wenzelm
# Date 1725909808 -7200
# Node ID 389e1bf96e052cc483c6b92eb3fa361b0c2b2e92
# Parent  2ef32d34ef1c999081479cc44e18ccddb12ab282
minor performance tuning;

diff -r 2ef32d34ef1c -r 389e1bf96e05 src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Mon Sep 09 19:51:16 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Mon Sep 09 21:23:28 2024 +0200
@@ -94,7 +94,11 @@
 
 fun output_markup (markup as (name, atts)) =
   if Markup.is_empty markup then Markup.no_output
-  else (XY ^ name ^ implode (map (fn p => Y ^ Properties.print_eq p) atts) ^ X, XYX);
+  else
+    let
+      val bgs = XY :: name :: fold_rev (fn p => cons Y o cons (Properties.print_eq p)) atts [X];
+      val en = XYX;
+    in (implode bgs, en) end;
 
 val output_markup_only = op ^ o output_markup;