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;