# HG changeset patch
# User wenzelm
# Date 1725901253 -7200
# Node ID b866d1510bd041da0c3519c6292e34011660b4ab
# Parent  0d92bd90be6c3627c542c66099c84bf365ad3a9d
clarified signature: more explicit type output_ops: default via print_mode;

diff -r 0d92bd90be6c -r b866d1510bd0 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 09 13:43:28 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 09 19:00:53 2024 +0200
@@ -66,10 +66,17 @@
   val big_list: string -> T list -> T
   val indent: int -> T -> T
   val unbreakable: T -> T
+  type output_ops =
+   {output: string -> Output.output * int,
+    escape: Output.output list -> string list,
+    markup: Markup.T -> Markup.output,
+    indent: string -> int -> Output.output,
+    margin: int}
+  val output_ops: int option -> output_ops
   val regularN: string
   val symbolicN: string
-  val output_buffer: int option -> T -> Buffer.T
-  val output: int option -> T -> Output.output list
+  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: T -> string
   val writeln: T -> unit
@@ -106,11 +113,6 @@
       (Library.get_first (Symtab.lookup (Synchronized.value modes)) (print_mode_value ()));
 end;
 
-fun mode_indent x y = #indent (get_mode ()) x y;
-
-val output_spaces = Output.output_width o Symbol.spaces;
-val buffer_output_spaces = Buffer.add o #1 o output_spaces;
-
 
 
 (** printing items: compound phrases, strings, and breaks **)
@@ -229,6 +231,29 @@
 
 (** formatting **)
 
+(* output operations: default via print_mode *)
+
+type output_ops =
+ {output: string -> Output.output * int,
+  escape: Output.output list -> string list,
+  markup: Markup.T -> Markup.output,
+  indent: string -> int -> Output.output,
+  margin: int};
+
+fun output_ops opt_margin : output_ops =
+  let
+    val {output, escape} = Output.get_mode ();
+    val {output = markup} = Markup.get_mode ();
+    val {indent} = get_mode ();
+    val margin = the_default ML_Pretty.default_margin opt_margin;
+  in {output = output, escape = escape, markup = markup, indent = indent, margin = margin} end;
+
+fun output_newline (ops: output_ops) = #1 (#output ops "\n");
+
+fun output_spaces (ops: output_ops) = #output ops o Symbol.spaces;
+fun output_spaces' ops = Buffer.add o #1 o output_spaces ops;
+
+
 (* formatted output *)
 
 local
@@ -241,8 +266,8 @@
   pos = 0,
   nl = 0};
 
-fun newline {tx, ind = _, pos = _, nl} : text =
- {tx = Buffer.add (Output.output "\n") tx,
+fun newline s {tx, ind = _, pos = _, nl} : text =
+ {tx = Buffer.add s tx,
   ind = Buffer.empty,
   pos = 0,
   nl = nl + 1};
@@ -259,16 +284,6 @@
   pos = pos + len,
   nl = nl};
 
-val blanks = string o output_spaces;
-
-fun indentation (buf, len) {tx, ind, pos, nl} : text =
-  let val s = Buffer.content buf in
-   {tx = Buffer.add (mode_indent s len) tx,
-    ind = Buffer.add s ind,
-    pos = pos + len,
-    nl = nl}
-  end;
-
 (*Add the lengths of the expressions until the next Break; if no Break then
   include "after", to account for text following this block.*)
 fun break_dist (Break _ :: _, _) = 0
@@ -307,7 +322,7 @@
 
 in
 
-fun output_tree make_length =
+fun output_tree (ops: output_ops) make_length =
   let
     fun out (T (ML_Pretty.PrettyBlock (ind, consistent, context, body))) =
           let
@@ -319,15 +334,28 @@
           in Block ((bg, en), consistent, indent, body', len) end
       | out (T (ML_Pretty.PrettyBreak (wd, ind))) = Break (false, long_nat wd, long_nat ind)
       | out (T ML_Pretty.PrettyLineBreak) = fbreak
-      | out (T (ML_Pretty.PrettyString s)) = Str (Output.output_width s ||> force_nat)
+      | out (T (ML_Pretty.PrettyString s)) = Str (#output ops s ||> force_nat)
       | out (T (ML_Pretty.PrettyStringWithWidth (s, n))) = Str (s, long_nat n);
   in out end;
 
-fun format_tree margin input =
+fun format_tree (ops: output_ops) input =
   let
+    val margin = #margin ops;
     val breakgain = margin div 20;     (*minimum added space required of a break*)
     val emergencypos = margin div 2;   (*position too far to right*)
 
+    val linebreak = newline (output_newline ops);
+    val blanks = string o output_spaces ops;
+    val blanks' = output_spaces' ops;
+
+    fun indentation (buf, len) {tx, ind, pos, nl} : text =
+      let val s = Buffer.content buf in
+       {tx = Buffer.add (#indent ops s len) tx,
+        ind = Buffer.add s ind,
+        pos = pos + len,
+        nl = nl}
+      end;
+
     (*es is list of expressions to print;
       blockin is the indentation of the current block;
       after is the width of the following context until next break.*)
@@ -339,8 +367,8 @@
                 val pos' = pos + indent;
                 val pos'' = pos' mod emergencypos;
                 val block' =
-                  if pos' < emergencypos then (ind |> buffer_output_spaces indent, pos')
-                  else (buffer_output_spaces pos'' Buffer.empty, pos'');
+                  if pos' < emergencypos then (ind |> blanks' indent, pos')
+                  else (blanks' pos'' Buffer.empty, pos'');
                 val d = break_dist (es, after)
                 val bes' = if consistent andalso pos + blen > margin - d then force_all bes else bes;
                 val btext: text = text
@@ -357,10 +385,10 @@
                 (if not force andalso
                     pos + wd <= Int.max (margin - break_dist (es, after), blockin + breakgain)
                  then text |> blanks wd  (*just insert wd blanks*)
-                 else text |> newline |> indentation block |> blanks ind)
+                 else text |> linebreak |> indentation block |> blanks ind)
           | Str str => format (es, block, after) (string str text));
   in
-    #tx (format ([output_tree true input], (Buffer.empty, 0), 0) empty)
+    #tx (format ([output_tree ops true input], (Buffer.empty, 0), 0) empty)
   end;
 
 end;
@@ -368,30 +396,30 @@
 
 (* special output *)
 
-fun buffer_markup m body =
-  let val (bg, en) = Markup.output m
-  in Buffer.add bg #> body #> Buffer.add en end;
+(*symbolic markup -- no formatting*)
+fun symbolic ops prt =
+  let
+    fun buffer_markup m body =
+      let val (bg, en) = #markup ops m
+      in Buffer.add bg #> body #> Buffer.add en end;
 
-(*symbolic markup -- no formatting*)
-val symbolic =
-  let
     fun out (Block ((bg, en), _, _, [], _)) = Buffer.add bg #> Buffer.add en
       | out (Block ((bg, en), consistent, indent, prts, _)) =
           Buffer.add bg #>
           buffer_markup (Markup.block consistent indent) (fold out prts) #>
           Buffer.add en
-      | out (Break (false, wd, ind)) = buffer_markup (Markup.break wd ind) (buffer_output_spaces wd)
-      | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
+      | out (Break (false, wd, ind)) = buffer_markup (Markup.break wd ind) (output_spaces' ops wd)
+      | out (Break (true, _, _)) = Buffer.add (output_newline ops)
       | out (Str (s, _)) = Buffer.add s;
-  in Buffer.build o out o output_tree false end;
+  in Buffer.build (out (output_tree ops false prt)) end;
 
 (*unformatted output*)
-val unformatted =
+fun unformatted ops prt =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
-      | out (Break (_, wd, _)) = buffer_output_spaces wd
+      | out (Break (_, wd, _)) = output_spaces' ops wd
       | out (Str (s, _)) = Buffer.add s;
-  in Buffer.build o out o output_tree false end;
+  in Buffer.build (out (output_tree ops false prt)) end;
 
 
 (* output interfaces *)
@@ -399,20 +427,34 @@
 val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";
 
-fun output_buffer margin prt =
+fun output_buffer ops prt =
   if print_mode_active symbolicN andalso not (print_mode_active regularN)
-  then symbolic prt
-  else format_tree (the_default ML_Pretty.default_margin margin) prt;
+  then symbolic ops prt
+  else format_tree ops prt;
 
 val output = Buffer.contents oo output_buffer;
-fun string_of_margin margin = implode o Output.escape o output (SOME margin);
-val string_of = implode o Output.escape o output NONE;
-val writeln = Output.writelns o Output.escape o output NONE;
+
+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;
 
-val symbolic_output = Buffer.contents o symbolic;
-val symbolic_string_of = implode o Output.escape o symbolic_output;
+fun writeln prt =
+  let val ops = output_ops NONE
+  in Output.writelns (#escape ops (output ops prt)) end;
+
+fun symbolic_output prt = Buffer.contents (symbolic (output_ops NONE) prt);
 
-val unformatted_string_of = implode o Output.escape o Buffer.contents o unformatted;
+fun symbolic_string_of prt =
+  let val ops = output_ops NONE
+  in implode (#escape ops (Buffer.contents (symbolic ops prt))) end;
+
+fun unformatted_string_of prt =
+  let val ops = output_ops NONE
+  in implode (#escape ops (Buffer.contents (unformatted ops prt))) end;
 
 
 (* chunks *)