--- a/src/Pure/PIDE/markup.ML Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/PIDE/markup.ML Thu Apr 24 22:45:04 2025 +0200
@@ -293,6 +293,7 @@
val no_output: output
val output: T -> output
val markup: T -> string -> string
+ val markup_strings: T -> string list -> string list
val markups: T list -> string -> string
val markup_report: string -> string
end;
@@ -898,6 +899,10 @@
fun markup m = output m |-> Library.enclose;
+fun markup_strings m =
+ let val (bg, en) = output m
+ in fn ss => [bg] @ ss @ [en] end;
+
val markups = fold_rev markup;
fun markup_report "" = ""