src/Pure/General/pretty.ML

   val symbolic_string_of: T -> string
   val unformatted_string_of: T -> string
   val output: output_ops -> T -> Bytes.T
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
+  val strings_of: T -> string list
   val pure_string_of: T -> string
   val writeln: T -> unit
   val writeln_urgent: T -> unit
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T

 fun output ops = if #symbolic ops then symbolic_output else format_tree ops;
 
 fun string_of_ops ops = Bytes.content o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
+fun strings_of prt = Bytes.contents (output (output_ops NONE) prt);
+
 val pure_string_of = string_of_ops (pure_output_ops NONE);
 
 fun gen_writeln urgent prt =
   (if urgent then Output.writelns_urgent else Output.writelns)
     (Bytes.contents (output (output_ops NONE) prt));