src/Pure/PIDE/markup.ML
changeset 82583 abd3885a3fcf
parent 82316 83584916b6d7
--- 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 "" = ""