# HG changeset patch
# User wenzelm
# Date 1725963744 -7200
# Node ID 793e490d7bd168566667e3a5e48902134534cf01
# Parent  b11bd8af381d269e32ecddaa5767483bf0550393
tuned signature;

diff -r b11bd8af381d -r 793e490d7bd1 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Tue Sep 10 12:05:37 2024 +0200
+++ b/src/Pure/General/pretty.ML	Tue Sep 10 12:22:24 2024 +0200
@@ -247,7 +247,7 @@
   let
     val {output, escape} = Output.get_mode ();
     val {markup, indent} = get_mode ();
-    val margin = the_default ML_Pretty.default_margin opt_margin;
+    val margin = ML_Pretty.get_margin opt_margin;
   in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end;
 
 fun markup_output_ops opt_margin : output_ops =
@@ -255,7 +255,7 @@
   escape = #escape Output.default_ops,
   markup = #markup markup_ops,
   indent = #indent markup_ops,
-  margin = the_default ML_Pretty.default_margin opt_margin};
+  margin = ML_Pretty.get_margin opt_margin};
 
 fun output_newline (ops: output_ops) = #1 (#output ops "\n");
 
diff -r b11bd8af381d -r 793e490d7bd1 src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Tue Sep 10 12:05:37 2024 +0200
+++ b/src/Pure/ML/ml_pretty.ML	Tue Sep 10 12:22:24 2024 +0200
@@ -19,6 +19,7 @@
   val prune: FixedInt.int -> pretty -> pretty
   val format: int -> pretty -> string
   val default_margin: int
+  val get_margin: int option -> int
   val string_of: pretty -> string
   val make_string_fn: string
 end;
@@ -70,6 +71,8 @@
 
 val default_margin = 76;
 
+val get_margin = the_default default_margin;
+
 
 (* make string *)