# HG changeset patch
# User wenzelm
# Date 1736004125 -3600
# Node ID 289ded3c342f2634143bec839924aba52c14498a
# Parent  114449035ec6b048668480931fa2e6be54b17a0d
tuned names: more uniform;

diff -r 114449035ec6 -r 289ded3c342f src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Jan 04 15:09:47 2025 +0100
+++ b/src/Pure/General/pretty.ML	Sat Jan 04 16:22:05 2025 +0100
@@ -341,7 +341,7 @@
 
 fun state_output (State (_, output)) = output;
 
-val empty_state = State ([], Bytes.empty);
+val init_state = State ([], Bytes.empty);
 
 fun add_state s (State (context, output)) =
   State (context, Bytes.add s output);
@@ -362,8 +362,8 @@
 
 type text = {main: state, line: state option, pos: int, nl: int};
 
-val empty: text = {main = empty_state, line = NONE, pos = 0, nl = 0};
-val empty_line: text = {main = empty_state, line = SOME empty_state, pos = 0, nl = 0};
+val init_no_line: text = {main = init_state, line = NONE, pos = 0, nl = 0};
+val init_line: text = {main = init_state, line = SOME init_state, pos = 0, nl = 0};
 
 fun string (s, len) {main, line, pos, nl} : text =
  {main = add_state s main,
@@ -429,7 +429,7 @@
                   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;
+              val line' = init_state |> fold add_state ss |> reopen_state main;
             in (main', SOME line') end;
       in {main = main', line = line', pos = pos, nl = nl + 1} end;
 
@@ -448,7 +448,7 @@
             val before' =
               if pos' < emergencypos
               then (Option.map (close_state o blanks_state indent) (#line text), pos')
-              else (Option.map (fn _ => blanks_state pos'' empty_state) (#line text), pos'');
+              else (Option.map (fn _ => blanks_state pos'' init_state) (#line text), pos'');
             val after' = break_dist (ts, after)
             val body' = body
               |> (consistent andalso pos + blen > margin - after') ? map force_break;
@@ -467,7 +467,7 @@
              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;
+    val init = if no_indent_markup then init_no_line else init_line;
   in
     result (format ([output_tree ops true input], (#line init, 0), 0) init)
   end;
diff -r 114449035ec6 -r 289ded3c342f src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Sat Jan 04 15:09:47 2025 +0100
+++ b/src/Pure/General/pretty.scala	Sat Jan 04 16:22:05 2025 +0100
@@ -163,34 +163,34 @@
   private val init_state: State = List(Result_Buffer())
 
   private sealed case class Text(
-    state: State = init_state,
+    main: State = init_state,
     pos: Double = 0.0,
     nl: Int = 0
   ) {
     def add(elem: Elem_Buffer): Text =
-      (state: @unchecked) match {
-        case res :: rest => copy(state = res.add(elem) :: rest)
+      (main: @unchecked) match {
+        case res :: rest => copy(main = res.add(elem) :: rest)
       }
 
     def push(m: Markup_Body): Text =
-      copy(state = Result_Buffer(markup = m) :: state)
+      copy(main = Result_Buffer(markup = m) :: main)
 
     def pop: Text =
-      (state: @unchecked) match {
-        case res1 :: res2 :: rest => copy(state = res2.add(res1.result_elem) :: rest)
+      (main: @unchecked) match {
+        case res1 :: res2 :: rest => copy(main = res2.add(res1.result_elem) :: rest)
       }
 
     def result: XML.Body =
-      (state: @unchecked) match {
+      (main: @unchecked) match {
         case List(res) if res.markup == no_markup => res.result_body
       }
 
-    def reset: Text = copy(state = init_state)
-    def restore(other: Text): Text = copy(state = other.state)
+    def reset: Text = copy(main = init_state)
+    def restore(other: Text): Text = copy(main = other.main)
 
     def string(s: String, len: Double): Text =
-      (state: @unchecked) match {
-        case res :: rest => copy(state = res.string(s) :: rest, pos = pos + len)
+      (main: @unchecked) match {
+        case res :: rest => copy(main = res.string(s) :: rest, pos = pos + len)
       }
     def blanks(wd: Int): Text = string(Symbol.spaces(wd), wd.toDouble)
     def newline: Text = string("\n", 0.0).copy(pos = 0.0, nl = nl + 1)