src/Pure/PIDE/markup.ML
changeset 80846 9ed32b8a03a9
parent 80827 2ef32d34ef1c
child 80858 a392351d1ed4
--- a/src/Pure/PIDE/markup.ML	Tue Sep 10 16:06:38 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Tue Sep 10 19:57:45 2024 +0200
@@ -864,9 +864,7 @@
 
 fun output m = if is_empty m then no_output else #output (get_mode ()) m;
 
-fun markup m =
-  let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode);
-  in Library.enclose bg en end;
+fun markup m = output m |-> Library.enclose;
 
 val markups = fold_rev markup;