tuned;
authorwenzelm
Wed, 01 Jan 2025 16:42:28 +0100
changeset 81701 600d1f17af68
parent 81700 5c90d1f3a44c
child 81702 dc105ee2d759
tuned;
src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Jan 01 16:33:35 2025 +0100
+++ b/src/Pure/General/pretty.ML	Wed Jan 01 16:42:28 2025 +0100
@@ -408,31 +408,30 @@
     val breakgain = margin div 20;     (*minimum added space required of a break*)
     val emergencypos = margin div 2;   (*position too far to right*)
 
-    val newline = output_newline ops;
-
+    fun blanks_state n state = add_state (#1 (output_spaces ops n)) state;
     val blanks = string o output_spaces ops;
-    fun blanks_state n state = add_state (#1 (output_spaces ops n)) state;
 
     val indent_markup = #indent_markup ops;
     val no_indent_markup = indent_markup = Markup.no_output;
 
-    fun break_indent (before_state, before_pos) ({main, nl, ...}: text) : text =
+    val break_state = add_state (output_newline ops);
+    fun break (state, pos) ({main, nl, ...}: text) : text =
       let
         val (main', line') =
           if no_indent_markup then
-            (main |> add_state newline |> add_state (Symbol.spaces before_pos), NONE)
+            (main |> break_state |> add_state (Symbol.spaces pos), NONE)
           else
             let
-              val ss = Bytes.contents (state_output (the before_state));
+              val ss = Bytes.contents (state_output (the state));
               val main' =
-                if null ss then main |> add_state newline
+                if null ss then main |> break_state
                 else
-                  main |> close_state |> add_state newline
+                  main |> close_state |> break_state
                   |> push_state indent_markup |> fold add_state ss |> pop_state
                   |> reopen_state main;
               val line' = empty_state |> fold add_state ss |> reopen_state main;
             in (main', SOME line') end;
-      in {main = main', line = line', pos = before_pos, nl = nl + 1} end;
+      in {main = main', line = line', pos = pos, nl = nl + 1} end;
 
     (*'before' is the indentation context of the current block*)
     (*'after' is the width of the input context until the next break*)
@@ -465,7 +464,7 @@
             (if not force andalso
                 pos + wd <= Int.max (margin - break_dist (ts, after), #2 before + breakgain)
              then text |> blanks wd  (*just insert wd blanks*)
-             else text |> break_indent before |> blanks ind)
+             else text |> break before |> blanks ind)
       | Str str :: ts => format (ts, before, after) (string str text));
 
     val init = if no_indent_markup then empty else empty_line;