# HG changeset patch
# User wenzelm
# Date 1725307253 -7200
# Node ID 9035d32b4af37d117859f030eacd020388c8a1e7
# Parent  7e39c785ca5d9e7cb33d1fd7ef426eb7faaaae74
clarified output_spaces, based on Output.output_width;
tuned add_spaces;

diff -r 7e39c785ca5d -r 9035d32b4af3 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Mon Sep 02 20:54:00 2024 +0200
+++ b/src/Pure/General/pretty.ML	Mon Sep 02 22:00:53 2024 +0200
@@ -107,8 +107,8 @@
 
 fun mode_indent x y = #indent (get_mode ()) x y;
 
-val output_spaces = Output.output o Symbol.spaces;
-val add_indent = Buffer.add o output_spaces;
+val output_spaces = Output.output_width o Symbol.spaces;
+val add_spaces = Buffer.add o #1 o output_spaces;
 
 
 
@@ -216,7 +216,7 @@
 
 fun unbreakable (Block (m, consistent, indent, es, len)) =
       Block (m, consistent, indent, map unbreakable es, len)
-  | unbreakable (Break (_, wd, _)) = Str (output_spaces wd, wd)
+  | unbreakable (Break (_, wd, _)) = Str (output_spaces wd)
   | unbreakable (e as Str _) = e;
 
 
@@ -253,7 +253,7 @@
   pos = pos + len,
   nl = nl};
 
-fun blanks wd = string (output_spaces wd, wd);
+val blanks = string o output_spaces;
 
 fun indentation (buf, len) {tx, ind, pos, nl} : text =
   let val s = Buffer.content buf in
@@ -295,8 +295,8 @@
                 val pos' = pos + indent;
                 val pos'' = pos' mod emergencypos;
                 val block' =
-                  if pos' < emergencypos then (ind |> add_indent indent, pos')
-                  else (add_indent pos'' Buffer.empty, pos'');
+                  if pos' < emergencypos then (ind |> add_spaces indent, pos')
+                  else (add_spaces 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
@@ -332,8 +332,7 @@
           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.add (output_spaces wd))
+      | out (Break (false, wd, ind)) = Buffer.markup (Markup.break wd ind) (add_spaces wd)
       | out (Break (true, _, _)) = Buffer.add (Output.output "\n")
       | out (Str (s, _)) = Buffer.add s;
   in Buffer.build o out end;
@@ -342,7 +341,7 @@
 val unformatted =
   let
     fun out (Block ((bg, en), _, _, prts, _)) = Buffer.add bg #> fold out prts #> Buffer.add en
-      | out (Break (_, wd, _)) = Buffer.add (output_spaces wd)
+      | out (Break (_, wd, _)) = add_spaces wd
       | out (Str (s, _)) = Buffer.add s;
   in Buffer.build o out end;