# HG changeset patch
# User wenzelm
# Date 1725911156 -7200
# Node ID 28f069b85eeaba883cb6c10f01fc54542c985523
# Parent  bdae6195a287321a81ae3dcaa6bb3390693de32f
tuned signature: more options;

diff -r bdae6195a287 -r 28f069b85eea src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 21:32:11 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 21:45:56 2024 +0200
@@ -74,6 +74,7 @@
     indent: string -> int -> Output.output,
     margin: int}
   val output_ops: int option -> output_ops
+  val markup_output_ops: int option -> output_ops
   val regularN: string
   val symbolicN: string
   val output_buffer: output_ops -> T -> Buffer.T
@@ -249,12 +250,12 @@
     val margin = the_default ML_Pretty.default_margin opt_margin;
   in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end;
 
-val markup_output_ops: output_ops =
+fun markup_output_ops opt_margin : output_ops =
  {output = #output Output.default_ops,
   escape = #escape Output.default_ops,
   markup = #markup markup_ops,
   indent = #indent markup_ops,
-  margin = ML_Pretty.default_margin};
+  margin = the_default ML_Pretty.default_margin opt_margin};
 
 fun output_newline (ops: output_ops) = #1 (#output ops "\n");
 
@@ -406,7 +407,7 @@
 (*symbolic markup -- no formatting*)
 val symbolic =
   let
-    val ops = markup_output_ops;
+    val ops = markup_output_ops NONE;
 
     fun buffer_markup m body =
       let val (bg, en) = #markup ops (YXML.output_markup m)