--- a/src/Pure/General/pretty.ML Wed Sep 11 21:41:33 2024 +0200
+++ b/src/Pure/General/pretty.ML Wed Sep 11 22:28:42 2024 +0200
@@ -77,6 +77,7 @@
val output: output_ops -> T -> Bytes.T
val string_of_ops: output_ops -> T -> string
val string_of: T -> string
+ val pure_string_of: T -> string
val writeln: T -> unit
val markup_chunks: Markup.T -> T list -> T
val chunks: T list -> T
@@ -428,6 +429,8 @@
fun string_of_ops ops = Bytes.content o output ops;
fun string_of prt = string_of_ops (output_ops NONE) prt;
+val pure_string_of = string_of_ops (pure_output_ops NONE);
+
fun writeln prt =
Output.writelns (Bytes.contents (output (output_ops NONE) prt));