| changeset 80789 | bcecb69f72fa |
| parent 78463 | c956b43749f0 |
| child 80821 | eb383d50564b |
--- a/src/Pure/PIDE/markup.ML Thu Aug 29 11:43:14 2024 +0200 +++ b/src/Pure/PIDE/markup.ML Thu Aug 29 17:47:29 2024 +0200 @@ -864,8 +864,8 @@ val enclose = output #-> Library.enclose; fun markup m = - let val (bg, en) = output m - in Library.enclose (Output.escape bg) (Output.escape en) end; + let val (bg, en) = output m |> apply2 (single #> Output.escape #> implode); + in Library.enclose bg en end; val markups = fold_rev markup;