--- a/src/Pure/General/pretty.ML Tue Sep 10 12:22:24 2024 +0200
+++ b/src/Pure/General/pretty.ML Tue Sep 10 12:34:32 2024 +0200
@@ -79,7 +79,7 @@
val symbolicN: string
val output_buffer: output_ops -> T -> Buffer.T
val output: output_ops -> T -> Output.output list
- val string_of_margin: int -> T -> string
+ val string_of_ops: output_ops -> T -> string
val string_of: T -> string
val writeln: T -> unit
val symbolic_output: T -> Output.output list
@@ -444,13 +444,8 @@
val output = Buffer.contents oo output_buffer;
-fun string_of_margin margin prt =
- let val ops = output_ops (SOME margin)
- in implode (#escape ops (output ops prt)) end;
-
-fun string_of prt =
- let val ops = output_ops NONE
- in implode (#escape ops (output ops prt)) end;
+fun string_of_ops ops = implode o #escape ops o output ops;
+fun string_of prt = string_of_ops (output_ops NONE) prt;
fun writeln prt =
let val ops = output_ops NONE
--- a/src/Pure/Thy/document_antiquotation.ML Tue Sep 10 12:22:24 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML Tue Sep 10 12:34:32 2024 +0200
@@ -84,7 +84,7 @@
fun format ctxt =
if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
- then Pretty.string_of_margin (Config.get ctxt thy_output_margin)
+ then Pretty.string_of_ops (Pretty.output_ops (SOME (Config.get ctxt thy_output_margin)))
else Pretty.unformatted_string_of;
fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;