# HG changeset patch
# User wenzelm
# Date 1725964472 -7200
# Node ID 1beb2dc3bf144b98065b13ad4a88fee40ebf45a4
# Parent  793e490d7bd168566667e3a5e48902134534cf01
clarified signature;

diff -r 793e490d7bd1 -r 1beb2dc3bf14 src/Pure/General/pretty.ML
--- 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
diff -r 793e490d7bd1 -r 1beb2dc3bf14 src/Pure/Thy/document_antiquotation.ML
--- 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;