From d1b6051db04e3ee94876f00379bb98b154bc530b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 18:34:57 +0300
Subject: [PATCH 1/8] Move most Pretty global state into state record to pass
 around

---
 src/ocamlutil/pretty.ml | 186 +++++++++++++++++++---------------------
 1 file changed, 86 insertions(+), 100 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 0d7f0678f..0221fa560 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -267,63 +267,69 @@ type align =
                                       deltaFromPrev of the next active align *)
     }
 
-(* We use references to avoid the need to pass data around all the time *)
-let aligns: align list refDLS =  (* The current stack of active alignment marks,
-                                 with the top at the head. Never empty.  *)
-  refDLS [{ gainBreak = 0; isTaken = ref false;
-         deltaFromPrev = ref 0; deltaToNext = ref 0; }]
+type state = {
+  aligns: align list refDLS;
+  (** The current stack of active alignment marks, with the top at the head. Never empty. *)
 
-let topAlignAbsCol = refDLS 0 (* The absolute column of the top alignment *)
+  topAlignAbsCol: int refDLS;
+  (** The absolute column of the top alignment *)
 
-let pushAlign (abscol: int) =
-  let topalign = List.hd @@ DLS.get aligns in
+  activeMarkups: int list refDLS;
+  (** We keep a list of active markup sections. For each one we keep the column we are in *)
+
+  breaks: bool ref list refDLS;
+  (** Keep a list of ref cells for the breaks, in the same order that we see them in the document *)
+
+  maxCol: int refDLS;
+  (** The maximum column that we should use *)
+
+  breakAllMode: bool refDLS;
+  (** Sometimes we take all the optional breaks *)
+}
+
+let create_state (): state = {
+  aligns = refDLS [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
+  topAlignAbsCol = refDLS 0;
+  activeMarkups = refDLS [];
+  breaks = refDLS [];
+  maxCol = refDLS 0;
+  breakAllMode = refDLS false;
+}
+
+let pushAlign ~state (abscol: int) =
+  let topalign = List.hd @@ DLS.get state.aligns in
   let (res : align) =
     { gainBreak = 0; isTaken = ref false;
       deltaFromPrev = topalign.deltaToNext; (* Share with the previous *)
       deltaToNext = ref 0; (* Allocate a new ref *)} in
-  DLS.set aligns (res :: DLS.get aligns);
-  let newdelta = abscol - DLS.get topAlignAbsCol in
+  DLS.set state.aligns (res :: DLS.get state.aligns);
+  let newdelta = abscol - DLS.get state.topAlignAbsCol in
   res.deltaFromPrev := newdelta;
-  DLS.set topAlignAbsCol abscol
+  DLS.set state.topAlignAbsCol abscol
 
-let popAlign () =
-  match DLS.get aligns with
+let popAlign ~state =
+  match DLS.get state.aligns with
     top :: t when t != [] ->
-      DLS.set aligns t;
-      DLS.set topAlignAbsCol (DLS.get topAlignAbsCol - !(top.deltaFromPrev))
+      DLS.set state.aligns t;
+      DLS.set state.topAlignAbsCol (DLS.get state.topAlignAbsCol - !(top.deltaFromPrev))
   | _ -> failwith "Unmatched unalign\n"
 
-(** We keep a list of active markup sections. For each one we keep the column
-   we are in *)
-let activeMarkups: int list refDLS = refDLS []
-
-
-(* Keep a list of ref cells for the breaks, in the same order that we see
-   them in the document *)
-let breaks: bool ref list refDLS = refDLS []
-
-(* The maximum column that we should use *)
-let maxCol = refDLS 0
-
-(* Sometimes we take all the optional breaks *)
-let breakAllMode = refDLS false
-
 (* We are taking a newline and moving left *)
-let newline () =
-  let topalign = List.hd (DLS.get aligns) in (* aligns is never empty *)
+let newline ~state =
+  let topalign = List.hd (DLS.get state.aligns) in (* aligns is never empty *)
   if debug then
     dbgprintf "Taking a newline: reseting gain of %d\n" topalign.gainBreak;
   topalign.gainBreak <- 0;        (* Erase the current break info *)
-  if (DLS.get breakAllMode) && DLS.get topAlignAbsCol < DLS.get maxCol then
-    DLS.set breakAllMode false;
-  DLS.get topAlignAbsCol                          (* This is the new column *)
+  if (DLS.get state.breakAllMode) && DLS.get state.topAlignAbsCol < DLS.get state.maxCol then
+    DLS.set state.breakAllMode false;
+  DLS.get state.topAlignAbsCol                          (* This is the new column *)
 
 
 
 (* Choose the align with the best gain. We ought to find a better way to
    keep the aligns sorted, especially since they gain never changes (when the
    align is the top align) *)
-let chooseBestGain () : align option =
+let chooseBestGain ~state : align option =
   let bestGain = ref 0 in
   let rec loop (breakingAlign: align option) = function
       [] -> breakingAlign
@@ -335,29 +341,29 @@ let chooseBestGain () : align option =
         end else
           loop breakingAlign resta
   in
-  loop None (DLS.get aligns)
+  loop None (DLS.get state.aligns)
 
 
 (* We have just advanced to a new column. See if we must take a line break *)
-let movingRight (abscol: int) : int =
+let movingRight ~state (abscol: int) : int =
   (* Keep taking the best break until we get back to the left of maxCol or no
      more are left *)
   let rec tryAgain abscol =
-    if abscol <= DLS.get maxCol then abscol else
+    if abscol <= DLS.get state.maxCol then abscol else
     begin
       if debug then
         dbgprintf "Looking for a break to take in column %d\n" abscol;
       (* Find the best gain there is out there *)
-      match if !fastMode then None else chooseBestGain () with
+      match if !fastMode then None else chooseBestGain ~state with
         None -> begin
           (* No breaks are available. Take all breaks from now on *)
-          DLS.set breakAllMode true;
+          DLS.set state.breakAllMode true;
           if debug then
             dbgprintf "Can't find any breaks\n";
           abscol
         end
       | Some breakingAlign -> begin
-          let topalign = List.hd (DLS.get aligns) in
+          let topalign = List.hd (DLS.get state.aligns) in
           let theGain = breakingAlign.gainBreak in
           assert (theGain > 0);
           if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain;
@@ -366,7 +372,7 @@ let movingRight (abscol: int) : int =
           if breakingAlign != topalign then begin
             breakingAlign.deltaToNext :=
                !(breakingAlign.deltaToNext) - theGain;
-            DLS.set topAlignAbsCol (DLS.get topAlignAbsCol - theGain)
+            DLS.set state.topAlignAbsCol (DLS.get state.topAlignAbsCol - theGain)
           end;
           tryAgain (abscol - theGain)
       end
@@ -399,68 +405,68 @@ let shallowAlign () =
 
 
 (* Pass the current absolute column and compute the new column *)
-let rec scan (abscol: int) (d: doc) : int =
+let rec scan ~state (abscol: int) (d: doc) : int =
   match d with
     Nil -> abscol
-  | Concat (d1, d2) -> scan (scan abscol d1) d2
+  | Concat (d1, d2) -> scan ~state (scan ~state abscol d1) d2
   | Text s when shallowAlign () ->
       let sl = String.length s in
       if debug then
         dbgprintf "Done string: %s from %d to %d\n" s abscol (abscol + sl);
-      movingRight (abscol + sl)
+      movingRight ~state (abscol + sl)
   | CText (d, s) ->
-      let abscol' = scan abscol d in
+      let abscol' = scan ~state abscol d in
       if shallowAlign () then begin
         let sl = String.length s in
         if debug then
           dbgprintf "Done string: %s from %d to %d\n" s abscol' (abscol' + sl);
-        movingRight (abscol' + sl)
+        movingRight ~state (abscol' + sl)
       end else
         abscol'
 
   | Align ->
-      pushAlign abscol;
+      pushAlign ~state abscol;
       if enterAlign () then
-        movingRight (abscol + 3) (* "..." *)
+        movingRight ~state (abscol + 3) (* "..." *)
       else
         abscol
 
-  | Unalign -> exitAlign (); popAlign (); abscol
+  | Unalign -> exitAlign (); popAlign ~state; abscol
 
   | Line when shallowAlign () -> (* A forced line break *)
-      if DLS.get activeMarkups != [] then
+      if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
-      newline ()
+      newline ~state
 
   | LeftFlush when shallowAlign ()  -> (* Keep cursor left-flushed *) 0
 
   | Break when shallowAlign () -> (* An optional line break. Always a space
                                      followed by an optional line break *)
-      if DLS.get activeMarkups != [] then
+      if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
       let takenref = ref false in
-      DLS.set breaks (takenref :: DLS.get breaks);
-      let topalign = List.hd (DLS.get aligns) in (* aligns is never empty *)
-      if DLS.get breakAllMode then begin
+      DLS.set state.breaks (takenref :: DLS.get state.breaks);
+      let topalign = List.hd (DLS.get state.aligns) in (* aligns is never empty *)
+      if DLS.get state.breakAllMode then begin
         takenref := true;
-        newline ()
+        newline ~state
       end else begin
         (* If there was a previous break there it stays not taken, forever.
            So we overwrite it. *)
         topalign.isTaken <- takenref;
-        topalign.gainBreak <- 1 + abscol - DLS.get topAlignAbsCol;
+        topalign.gainBreak <- 1 + abscol - DLS.get state.topAlignAbsCol;
         if debug then
           dbgprintf "Registering a break at %d with gain %d\n"
             (1 + abscol) topalign.gainBreak;
-        movingRight (1 + abscol)
+        movingRight ~state (1 + abscol)
       end
 
-  | Mark -> DLS.set activeMarkups (abscol :: DLS.get activeMarkups);
+  | Mark -> DLS.set state.activeMarkups (abscol :: DLS.get state.activeMarkups);
             abscol
 
   | Unmark -> begin
-      match DLS.get activeMarkups with
-        old :: rest -> DLS.set activeMarkups rest;
+      match DLS.get state.activeMarkups with
+        old :: rest -> DLS.set state.activeMarkups rest;
                        old
       | [] -> failwith "Too many unmark"
   end
@@ -473,7 +479,7 @@ let rec scan (abscol: int) (d: doc) : int =
 let countNewLines = refDLS 0
 
 (* The actual function that takes a document and prints it *)
-let emitDoc
+let emitDoc ~state
     (emitString: string -> int -> unit) (* emit a number of copies of a
                                            string *)
     (d: doc) =
@@ -546,10 +552,10 @@ let emitDoc
     | Line when shallowAlign ()  -> cont (newline ())
     | LeftFlush when shallowAlign () -> wantIndent := false;  cont (0)
     | Break when shallowAlign () -> begin
-        match DLS.get breaks with
+        match DLS.get state.breaks with
           [] -> failwith "Break without a takenref"
         | istaken :: rest ->
-            DLS.set breaks rest; (* Consume the break *)
+            DLS.set state.breaks rest; (* Consume the break *)
             if !istaken then cont (newline ())
             else begin
 	      indentIfNeeded ();
@@ -559,12 +565,12 @@ let emitDoc
     end
 
     | Mark ->
-        DLS.set activeMarkups (abscol :: DLS.get activeMarkups);
+        DLS.set state.activeMarkups (abscol :: DLS.get state.activeMarkups);
         cont abscol
 
     | Unmark -> begin
-        match DLS.get activeMarkups with
-          old :: rest -> DLS.set activeMarkups rest;
+        match DLS.get state.activeMarkups with
+          old :: rest -> DLS.set state.activeMarkups rest;
                          cont old
         | [] -> failwith "Unmark without a mark"
     end
@@ -577,36 +583,16 @@ let emitDoc
 
 
 let print_with_state ~width f =
-  (* Save some parameters, to allow for nested calls of these routines. *)
-  let old_maxCol = DLS.get maxCol in
-  DLS.set maxCol width;
-  let old_breaks = DLS.get breaks in
-  DLS.set breaks [];
-  let old_activeMarkups = DLS.get activeMarkups in
-  DLS.set activeMarkups [];
   let old_alignDepth = DLS.get alignDepth in
   DLS.set alignDepth 0;
-  let old_aligns = DLS.get aligns in
-  DLS.set aligns [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
-  let old_topAlignAbsCol = DLS.get topAlignAbsCol in
-  DLS.set topAlignAbsCol 0;
-  let old_breakAllMode = DLS.get breakAllMode in
-  DLS.set breakAllMode false;
+  let state = create_state () in
+  DLS.set state.maxCol width;
 
   let finally () =
-    DLS.set maxCol old_maxCol;
-    (* We must do this especially if we don't do emit
-       (which consumes breaks) because otherwise we waste
-       memory *)
-    DLS.set breaks old_breaks;
-    DLS.set activeMarkups old_activeMarkups;
     DLS.set alignDepth old_alignDepth;
-    DLS.set aligns old_aligns;
-    DLS.set topAlignAbsCol old_topAlignAbsCol;
-    DLS.set breakAllMode old_breakAllMode
   in
 
-  match f () with
+  match f ~state with
   | r ->
     finally ();
     r
@@ -618,10 +604,10 @@ let print_with_state ~width f =
 (* Print a document on a channel *)
 let fprint (chn: out_channel) ~(width: int) doc =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
-  print_with_state ~width (fun () ->
-      ignore (scan 0 doc);
-      DLS.set breaks @@ List.rev (DLS.get breaks);
-      emitDoc (fun s nrcopies ->
+  print_with_state ~width (fun ~state ->
+      ignore (scan ~state 0 doc);
+      DLS.set state.breaks @@ List.rev (DLS.get state.breaks);
+      emitDoc ~state (fun s nrcopies ->
           for _ = 1 to nrcopies do
             output_string chn s
           done
@@ -631,15 +617,15 @@ let fprint (chn: out_channel) ~(width: int) doc =
 (* Print the document to a string *)
 let sprint ~(width : int)  doc : string =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
-  print_with_state ~width (fun () ->
-      ignore (scan 0 doc);
-      DLS.set breaks @@ List.rev (DLS.get breaks);
+  print_with_state ~width (fun ~state ->
+      ignore (scan ~state 0 doc);
+      DLS.set state.breaks @@ List.rev (DLS.get state.breaks);
       let buf = Buffer.create 1024 in
       let rec add_n_strings str num =
         if num <= 0 then ()
         else begin Buffer.add_string buf str; add_n_strings str (num - 1) end
       in
-      emitDoc add_n_strings doc;
+      emitDoc ~state add_n_strings doc;
       Buffer.contents buf
     )
 

From d7f353e91d1e72d26fb260684025cc31298cba6b Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 18:51:18 +0300
Subject: [PATCH 2/8] Remove Pretty.alignDepth global state

---
 src/ocamlutil/pretty.ml | 55 +++++++++++++++++------------------------
 1 file changed, 22 insertions(+), 33 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 0221fa560..946d6a636 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -285,6 +285,8 @@ type state = {
 
   breakAllMode: bool refDLS;
   (** Sometimes we take all the optional breaks *)
+
+  alignDepth: int refDLS;
 }
 
 let create_state (): state = {
@@ -294,6 +296,7 @@ let create_state (): state = {
   breaks = refDLS [];
   maxCol = refDLS 0;
   breakAllMode = refDLS false;
+  alignDepth = refDLS 0;
 }
 
 let pushAlign ~state (abscol: int) =
@@ -385,22 +388,21 @@ let movingRight ~state (abscol: int) : int =
    have properly nested align/unalign pairs. When the nesting depth surpasses
    !printDepth then we print ... and we skip until the matching unalign *)
 let printDepth = ref 10000000 (* WRW: must see whole thing *)
-let alignDepth = refDLS 0
 
 let useAlignDepth = true
 
 (** Start an align. Return true if we have just passed the threshhold *)
-let enterAlign () =
+let enterAlign alignDepth =
   incrDLS alignDepth;
   useAlignDepth && DLS.get alignDepth = !printDepth + 1
 
 (** Exit an align *)
-let exitAlign () =
+let exitAlign alignDepth =
   decrDLS alignDepth
 
 (** See if we are at a low-enough align level (and we should be printing
    normally) *)
-let shallowAlign () =
+let shallowAlign alignDepth =
   not useAlignDepth || DLS.get alignDepth <= !printDepth
 
 
@@ -409,14 +411,14 @@ let rec scan ~state (abscol: int) (d: doc) : int =
   match d with
     Nil -> abscol
   | Concat (d1, d2) -> scan ~state (scan ~state abscol d1) d2
-  | Text s when shallowAlign () ->
+  | Text s when shallowAlign state.alignDepth ->
       let sl = String.length s in
       if debug then
         dbgprintf "Done string: %s from %d to %d\n" s abscol (abscol + sl);
       movingRight ~state (abscol + sl)
   | CText (d, s) ->
       let abscol' = scan ~state abscol d in
-      if shallowAlign () then begin
+      if shallowAlign state.alignDepth then begin
         let sl = String.length s in
         if debug then
           dbgprintf "Done string: %s from %d to %d\n" s abscol' (abscol' + sl);
@@ -426,21 +428,21 @@ let rec scan ~state (abscol: int) (d: doc) : int =
 
   | Align ->
       pushAlign ~state abscol;
-      if enterAlign () then
+      if enterAlign state.alignDepth then
         movingRight ~state (abscol + 3) (* "..." *)
       else
         abscol
 
-  | Unalign -> exitAlign (); popAlign ~state; abscol
+  | Unalign -> exitAlign state.alignDepth; popAlign ~state; abscol
 
-  | Line when shallowAlign () -> (* A forced line break *)
+  | Line when shallowAlign state.alignDepth -> (* A forced line break *)
       if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
       newline ~state
 
-  | LeftFlush when shallowAlign ()  -> (* Keep cursor left-flushed *) 0
+  | LeftFlush when shallowAlign state.alignDepth  -> (* Keep cursor left-flushed *) 0
 
-  | Break when shallowAlign () -> (* An optional line break. Always a space
+  | Break when shallowAlign state.alignDepth -> (* An optional line break. Always a space
                                      followed by an optional line break *)
       if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
@@ -516,7 +518,7 @@ let emitDoc ~state
     | Concat (d1, d2) ->
         loopCont abscol d1 (fun abscol' -> loopCont abscol' d2 cont)
 
-    | Text s when shallowAlign () ->
+    | Text s when shallowAlign state.alignDepth ->
         let sl = String.length s in
 	indentIfNeeded ();
         emitString s 1;
@@ -525,7 +527,7 @@ let emitDoc ~state
     | CText (d, s) ->
         loopCont abscol d
           (fun abscol' ->
-            if shallowAlign () then
+            if shallowAlign state.alignDepth then
               let sl = String.length s in
 	      indentIfNeeded ();
               emitString s 1;
@@ -535,7 +537,7 @@ let emitDoc ~state
 
     | Align ->
         aligns := (abscol :: !aligns);
-        if enterAlign () then begin
+        if enterAlign state.alignDepth then begin
           indentIfNeeded ();
           emitString "..." 1;
           cont (abscol + 3)
@@ -546,12 +548,12 @@ let emitDoc ~state
         match !aligns with
           [] -> failwith "Unmatched unalign"
         | _ :: rest ->
-            exitAlign ();
+            exitAlign state.alignDepth;
             aligns := rest; cont abscol
     end
-    | Line when shallowAlign ()  -> cont (newline ())
-    | LeftFlush when shallowAlign () -> wantIndent := false;  cont (0)
-    | Break when shallowAlign () -> begin
+    | Line when shallowAlign state.alignDepth  -> cont (newline ())
+    | LeftFlush when shallowAlign state.alignDepth -> wantIndent := false;  cont (0)
+    | Break when shallowAlign state.alignDepth -> begin
         match DLS.get state.breaks with
           [] -> failwith "Break without a takenref"
         | istaken :: rest ->
@@ -583,23 +585,9 @@ let emitDoc ~state
 
 
 let print_with_state ~width f =
-  let old_alignDepth = DLS.get alignDepth in
-  DLS.set alignDepth 0;
   let state = create_state () in
   DLS.set state.maxCol width;
-
-  let finally () =
-    DLS.set alignDepth old_alignDepth;
-  in
-
-  match f ~state with
-  | r ->
-    finally ();
-    r
-  | exception e ->
-    let bt = Printexc.get_raw_backtrace () in
-    finally ();
-    Printexc.raise_with_backtrace e bt
+  f ~state
 
 (* Print a document on a channel *)
 let fprint (chn: out_channel) ~(width: int) doc =
@@ -640,6 +628,7 @@ let gprintf (finish : doc -> 'b)
             (format : ('a, unit, doc, 'b) format4) : 'a =
   let format = string_of_format format in
 
+  let alignDepth = refDLS 0 in
   (* Record the starting align depth *)
   let startAlignDepth = DLS.get alignDepth in
   (* Special concatenation functions *)

From f635dfbae32a35e0c0bb314a6bf8db1a8d3677ef Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 18:53:26 +0300
Subject: [PATCH 3/8] Change Pretty.alignDepth via state record

---
 src/ocamlutil/pretty.ml | 42 ++++++++++++++++++++---------------------
 1 file changed, 21 insertions(+), 21 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 946d6a636..326e36d0b 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -392,18 +392,18 @@ let printDepth = ref 10000000 (* WRW: must see whole thing *)
 let useAlignDepth = true
 
 (** Start an align. Return true if we have just passed the threshhold *)
-let enterAlign alignDepth =
-  incrDLS alignDepth;
-  useAlignDepth && DLS.get alignDepth = !printDepth + 1
+let enterAlign ~state =
+  incrDLS state.alignDepth;
+  useAlignDepth && DLS.get state.alignDepth = !printDepth + 1
 
 (** Exit an align *)
-let exitAlign alignDepth =
-  decrDLS alignDepth
+let exitAlign ~state =
+  decrDLS state.alignDepth
 
 (** See if we are at a low-enough align level (and we should be printing
    normally) *)
-let shallowAlign alignDepth =
-  not useAlignDepth || DLS.get alignDepth <= !printDepth
+let shallowAlign ~state =
+  not useAlignDepth || DLS.get state.alignDepth <= !printDepth
 
 
 (* Pass the current absolute column and compute the new column *)
@@ -411,14 +411,14 @@ let rec scan ~state (abscol: int) (d: doc) : int =
   match d with
     Nil -> abscol
   | Concat (d1, d2) -> scan ~state (scan ~state abscol d1) d2
-  | Text s when shallowAlign state.alignDepth ->
+  | Text s when shallowAlign ~state ->
       let sl = String.length s in
       if debug then
         dbgprintf "Done string: %s from %d to %d\n" s abscol (abscol + sl);
       movingRight ~state (abscol + sl)
   | CText (d, s) ->
       let abscol' = scan ~state abscol d in
-      if shallowAlign state.alignDepth then begin
+      if shallowAlign ~state then begin
         let sl = String.length s in
         if debug then
           dbgprintf "Done string: %s from %d to %d\n" s abscol' (abscol' + sl);
@@ -428,21 +428,21 @@ let rec scan ~state (abscol: int) (d: doc) : int =
 
   | Align ->
       pushAlign ~state abscol;
-      if enterAlign state.alignDepth then
+      if enterAlign ~state then
         movingRight ~state (abscol + 3) (* "..." *)
       else
         abscol
 
-  | Unalign -> exitAlign state.alignDepth; popAlign ~state; abscol
+  | Unalign -> exitAlign ~state; popAlign ~state; abscol
 
-  | Line when shallowAlign state.alignDepth -> (* A forced line break *)
+  | Line when shallowAlign ~state -> (* A forced line break *)
       if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
       newline ~state
 
-  | LeftFlush when shallowAlign state.alignDepth  -> (* Keep cursor left-flushed *) 0
+  | LeftFlush when shallowAlign ~state  -> (* Keep cursor left-flushed *) 0
 
-  | Break when shallowAlign state.alignDepth -> (* An optional line break. Always a space
+  | Break when shallowAlign ~state -> (* An optional line break. Always a space
                                      followed by an optional line break *)
       if DLS.get state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
@@ -518,7 +518,7 @@ let emitDoc ~state
     | Concat (d1, d2) ->
         loopCont abscol d1 (fun abscol' -> loopCont abscol' d2 cont)
 
-    | Text s when shallowAlign state.alignDepth ->
+    | Text s when shallowAlign ~state ->
         let sl = String.length s in
 	indentIfNeeded ();
         emitString s 1;
@@ -527,7 +527,7 @@ let emitDoc ~state
     | CText (d, s) ->
         loopCont abscol d
           (fun abscol' ->
-            if shallowAlign state.alignDepth then
+            if shallowAlign ~state then
               let sl = String.length s in
 	      indentIfNeeded ();
               emitString s 1;
@@ -537,7 +537,7 @@ let emitDoc ~state
 
     | Align ->
         aligns := (abscol :: !aligns);
-        if enterAlign state.alignDepth then begin
+        if enterAlign ~state then begin
           indentIfNeeded ();
           emitString "..." 1;
           cont (abscol + 3)
@@ -548,12 +548,12 @@ let emitDoc ~state
         match !aligns with
           [] -> failwith "Unmatched unalign"
         | _ :: rest ->
-            exitAlign state.alignDepth;
+            exitAlign ~state;
             aligns := rest; cont abscol
     end
-    | Line when shallowAlign state.alignDepth  -> cont (newline ())
-    | LeftFlush when shallowAlign state.alignDepth -> wantIndent := false;  cont (0)
-    | Break when shallowAlign state.alignDepth -> begin
+    | Line when shallowAlign ~state  -> cont (newline ())
+    | LeftFlush when shallowAlign ~state -> wantIndent := false;  cont (0)
+    | Break when shallowAlign ~state -> begin
         match DLS.get state.breaks with
           [] -> failwith "Break without a takenref"
         | istaken :: rest ->

From c45dedeed3e6e5361aff70e9f25fd057b2faf497 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 18:54:00 +0300
Subject: [PATCH 4/8] Remove startAlignDepth in Pretty

---
 src/ocamlutil/pretty.ml | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 326e36d0b..3ee669299 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -629,8 +629,6 @@ let gprintf (finish : doc -> 'b)
   let format = string_of_format format in
 
   let alignDepth = refDLS 0 in
-  (* Record the starting align depth *)
-  let startAlignDepth = DLS.get alignDepth in
   (* Special concatenation functions *)
   let dconcat (acc: doc) (another: doc) =
     if DLS.get alignDepth > !printDepth then acc else acc ++ another in
@@ -640,7 +638,7 @@ let gprintf (finish : doc -> 'b)
   in
   (* Special finish function *)
   let dfinish (dc: doc) : 'b =
-    if DLS.get alignDepth <> startAlignDepth then
+    if DLS.get alignDepth <> 0 then
       prerr_string ("Unmatched align/unalign in " ^ format ^ "\n");
     finish dc
   in

From d81d54f090fde1e6806bc87520d0d1ba3a02a284 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 19:00:58 +0300
Subject: [PATCH 5/8] Replace refDLS with ref in Pretty

Since all of these refs have local scope.
---
 src/ocamlutil/pretty.ml | 120 ++++++++++++++++++++--------------------
 1 file changed, 60 insertions(+), 60 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 3ee669299..3b92aff9a 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -268,64 +268,64 @@ type align =
     }
 
 type state = {
-  aligns: align list refDLS;
+  aligns: align list ref;
   (** The current stack of active alignment marks, with the top at the head. Never empty. *)
 
-  topAlignAbsCol: int refDLS;
+  topAlignAbsCol: int ref;
   (** The absolute column of the top alignment *)
 
-  activeMarkups: int list refDLS;
+  activeMarkups: int list ref;
   (** We keep a list of active markup sections. For each one we keep the column we are in *)
 
-  breaks: bool ref list refDLS;
+  breaks: bool ref list ref;
   (** Keep a list of ref cells for the breaks, in the same order that we see them in the document *)
 
-  maxCol: int refDLS;
+  maxCol: int ref;
   (** The maximum column that we should use *)
 
-  breakAllMode: bool refDLS;
+  breakAllMode: bool ref;
   (** Sometimes we take all the optional breaks *)
 
-  alignDepth: int refDLS;
+  alignDepth: int ref;
 }
 
 let create_state (): state = {
-  aligns = refDLS [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
-  topAlignAbsCol = refDLS 0;
-  activeMarkups = refDLS [];
-  breaks = refDLS [];
-  maxCol = refDLS 0;
-  breakAllMode = refDLS false;
-  alignDepth = refDLS 0;
+  aligns = ref [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
+  topAlignAbsCol = ref 0;
+  activeMarkups = ref [];
+  breaks = ref [];
+  maxCol = ref 0;
+  breakAllMode = ref false;
+  alignDepth = ref 0;
 }
 
 let pushAlign ~state (abscol: int) =
-  let topalign = List.hd @@ DLS.get state.aligns in
+  let topalign = List.hd @@ !(state.aligns) in
   let (res : align) =
     { gainBreak = 0; isTaken = ref false;
       deltaFromPrev = topalign.deltaToNext; (* Share with the previous *)
       deltaToNext = ref 0; (* Allocate a new ref *)} in
-  DLS.set state.aligns (res :: DLS.get state.aligns);
-  let newdelta = abscol - DLS.get state.topAlignAbsCol in
+  state.aligns := (res :: !(state.aligns));
+  let newdelta = abscol - !(state.topAlignAbsCol) in
   res.deltaFromPrev := newdelta;
-  DLS.set state.topAlignAbsCol abscol
+  state.topAlignAbsCol := abscol
 
 let popAlign ~state =
-  match DLS.get state.aligns with
+  match !(state.aligns) with
     top :: t when t != [] ->
-      DLS.set state.aligns t;
-      DLS.set state.topAlignAbsCol (DLS.get state.topAlignAbsCol - !(top.deltaFromPrev))
+      state.aligns := t;
+      state.topAlignAbsCol := (!(state.topAlignAbsCol) - !(top.deltaFromPrev))
   | _ -> failwith "Unmatched unalign\n"
 
 (* We are taking a newline and moving left *)
 let newline ~state =
-  let topalign = List.hd (DLS.get state.aligns) in (* aligns is never empty *)
+  let topalign = List.hd (!(state.aligns)) in (* aligns is never empty *)
   if debug then
     dbgprintf "Taking a newline: reseting gain of %d\n" topalign.gainBreak;
   topalign.gainBreak <- 0;        (* Erase the current break info *)
-  if (DLS.get state.breakAllMode) && DLS.get state.topAlignAbsCol < DLS.get state.maxCol then
-    DLS.set state.breakAllMode false;
-  DLS.get state.topAlignAbsCol                          (* This is the new column *)
+  if (!(state.breakAllMode)) && !(state.topAlignAbsCol) < !(state.maxCol) then
+    state.breakAllMode := false;
+  !(state.topAlignAbsCol)                          (* This is the new column *)
 
 
 
@@ -344,7 +344,7 @@ let chooseBestGain ~state : align option =
         end else
           loop breakingAlign resta
   in
-  loop None (DLS.get state.aligns)
+  loop None (!(state.aligns))
 
 
 (* We have just advanced to a new column. See if we must take a line break *)
@@ -352,7 +352,7 @@ let movingRight ~state (abscol: int) : int =
   (* Keep taking the best break until we get back to the left of maxCol or no
      more are left *)
   let rec tryAgain abscol =
-    if abscol <= DLS.get state.maxCol then abscol else
+    if abscol <= !(state.maxCol) then abscol else
     begin
       if debug then
         dbgprintf "Looking for a break to take in column %d\n" abscol;
@@ -360,13 +360,13 @@ let movingRight ~state (abscol: int) : int =
       match if !fastMode then None else chooseBestGain ~state with
         None -> begin
           (* No breaks are available. Take all breaks from now on *)
-          DLS.set state.breakAllMode true;
+          state.breakAllMode := true;
           if debug then
             dbgprintf "Can't find any breaks\n";
           abscol
         end
       | Some breakingAlign -> begin
-          let topalign = List.hd (DLS.get state.aligns) in
+          let topalign = List.hd (!(state.aligns)) in
           let theGain = breakingAlign.gainBreak in
           assert (theGain > 0);
           if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain;
@@ -375,7 +375,7 @@ let movingRight ~state (abscol: int) : int =
           if breakingAlign != topalign then begin
             breakingAlign.deltaToNext :=
                !(breakingAlign.deltaToNext) - theGain;
-            DLS.set state.topAlignAbsCol (DLS.get state.topAlignAbsCol - theGain)
+            state.topAlignAbsCol := (!(state.topAlignAbsCol) - theGain)
           end;
           tryAgain (abscol - theGain)
       end
@@ -393,17 +393,17 @@ let useAlignDepth = true
 
 (** Start an align. Return true if we have just passed the threshhold *)
 let enterAlign ~state =
-  incrDLS state.alignDepth;
-  useAlignDepth && DLS.get state.alignDepth = !printDepth + 1
+  incr state.alignDepth;
+  useAlignDepth && !(state.alignDepth) = !printDepth + 1
 
 (** Exit an align *)
 let exitAlign ~state =
-  decrDLS state.alignDepth
+  decr state.alignDepth
 
 (** See if we are at a low-enough align level (and we should be printing
    normally) *)
 let shallowAlign ~state =
-  not useAlignDepth || DLS.get state.alignDepth <= !printDepth
+  not useAlignDepth || !(state.alignDepth) <= !printDepth
 
 
 (* Pass the current absolute column and compute the new column *)
@@ -436,7 +436,7 @@ let rec scan ~state (abscol: int) (d: doc) : int =
   | Unalign -> exitAlign ~state; popAlign ~state; abscol
 
   | Line when shallowAlign ~state -> (* A forced line break *)
-      if DLS.get state.activeMarkups != [] then
+      if !(state.activeMarkups) != [] then
         failwith "Line breaks inside markup sections";
       newline ~state
 
@@ -444,31 +444,31 @@ let rec scan ~state (abscol: int) (d: doc) : int =
 
   | Break when shallowAlign ~state -> (* An optional line break. Always a space
                                      followed by an optional line break *)
-      if DLS.get state.activeMarkups != [] then
+      if !(state.activeMarkups) != [] then
         failwith "Line breaks inside markup sections";
       let takenref = ref false in
-      DLS.set state.breaks (takenref :: DLS.get state.breaks);
-      let topalign = List.hd (DLS.get state.aligns) in (* aligns is never empty *)
-      if DLS.get state.breakAllMode then begin
+      state.breaks := (takenref :: !(state.breaks));
+      let topalign = List.hd (!(state.aligns)) in (* aligns is never empty *)
+      if !(state.breakAllMode) then begin
         takenref := true;
         newline ~state
       end else begin
         (* If there was a previous break there it stays not taken, forever.
            So we overwrite it. *)
         topalign.isTaken <- takenref;
-        topalign.gainBreak <- 1 + abscol - DLS.get state.topAlignAbsCol;
+        topalign.gainBreak <- 1 + abscol - !(state.topAlignAbsCol);
         if debug then
           dbgprintf "Registering a break at %d with gain %d\n"
             (1 + abscol) topalign.gainBreak;
         movingRight ~state (1 + abscol)
       end
 
-  | Mark -> DLS.set state.activeMarkups (abscol :: DLS.get state.activeMarkups);
+  | Mark -> state.activeMarkups := (abscol :: !(state.activeMarkups));
             abscol
 
   | Unmark -> begin
-      match DLS.get state.activeMarkups with
-        old :: rest -> DLS.set state.activeMarkups rest;
+      match !(state.activeMarkups) with
+        old :: rest -> state.activeMarkups := rest;
                        old
       | [] -> failwith "Too many unmark"
   end
@@ -554,10 +554,10 @@ let emitDoc ~state
     | Line when shallowAlign ~state  -> cont (newline ())
     | LeftFlush when shallowAlign ~state -> wantIndent := false;  cont (0)
     | Break when shallowAlign ~state -> begin
-        match DLS.get state.breaks with
+        match !(state.breaks) with
           [] -> failwith "Break without a takenref"
         | istaken :: rest ->
-            DLS.set state.breaks rest; (* Consume the break *)
+            state.breaks := rest; (* Consume the break *)
             if !istaken then cont (newline ())
             else begin
 	      indentIfNeeded ();
@@ -567,12 +567,12 @@ let emitDoc ~state
     end
 
     | Mark ->
-        DLS.set state.activeMarkups (abscol :: DLS.get state.activeMarkups);
+        state.activeMarkups := (abscol :: !(state.activeMarkups));
         cont abscol
 
     | Unmark -> begin
-        match DLS.get state.activeMarkups with
-          old :: rest -> DLS.set state.activeMarkups rest;
+        match !(state.activeMarkups) with
+          old :: rest -> state.activeMarkups := rest;
                          cont old
         | [] -> failwith "Unmark without a mark"
     end
@@ -586,7 +586,7 @@ let emitDoc ~state
 
 let print_with_state ~width f =
   let state = create_state () in
-  DLS.set state.maxCol width;
+  state.maxCol := width;
   f ~state
 
 (* Print a document on a channel *)
@@ -594,7 +594,7 @@ let fprint (chn: out_channel) ~(width: int) doc =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
   print_with_state ~width (fun ~state ->
       ignore (scan ~state 0 doc);
-      DLS.set state.breaks @@ List.rev (DLS.get state.breaks);
+      state.breaks := List.rev (!(state.breaks));
       emitDoc ~state (fun s nrcopies ->
           for _ = 1 to nrcopies do
             output_string chn s
@@ -607,7 +607,7 @@ let sprint ~(width : int)  doc : string =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
   print_with_state ~width (fun ~state ->
       ignore (scan ~state 0 doc);
-      DLS.set state.breaks @@ List.rev (DLS.get state.breaks);
+      state.breaks := List.rev (!(state.breaks));
       let buf = Buffer.create 1024 in
       let rec add_n_strings str num =
         if num <= 0 then ()
@@ -628,17 +628,17 @@ let gprintf (finish : doc -> 'b)
             (format : ('a, unit, doc, 'b) format4) : 'a =
   let format = string_of_format format in
 
-  let alignDepth = refDLS 0 in
+  let alignDepth = ref 0 in
   (* Special concatenation functions *)
   let dconcat (acc: doc) (another: doc) =
-    if DLS.get alignDepth > !printDepth then acc else acc ++ another in
+    if !alignDepth > !printDepth then acc else acc ++ another in
   let dctext1 (acc: doc) (str: string) =
-    if DLS.get alignDepth > !printDepth then acc else
+    if !alignDepth > !printDepth then acc else
     CText(acc, str)
   in
   (* Special finish function *)
   let dfinish (dc: doc) : 'b =
-    if DLS.get alignDepth <> 0 then
+    if !alignDepth <> 0 then
       prerr_string ("Unmatched align/unalign in " ^ format ^ "\n");
     finish dc
   in
@@ -760,20 +760,20 @@ let gprintf (finish : doc -> 'b)
                                         (* Now the special format characters *)
             '[' ->                      (* align *)
               let newacc =
-                if DLS.get alignDepth > !printDepth then
+                if !alignDepth > !printDepth then
                   acc
-                else if DLS.get alignDepth = !printDepth then
+                else if !alignDepth = !printDepth then
                   CText(acc, "...")
                 else
                   acc ++ align
               in
-              incrDLS alignDepth;
+              incr alignDepth;
               collect newacc (i + 2)
 
           | ']' ->                        (* unalign *)
-              decrDLS alignDepth;
+              decr alignDepth;
               let newacc =
-                if DLS.get alignDepth >= !printDepth then
+                if !alignDepth >= !printDepth then
                   acc
                 else
                   acc ++ unalign

From eb3cf1b108cf70f6866c41a6f2df786497c6bb6f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 19:02:36 +0300
Subject: [PATCH 6/8] Remove refDLS and friends from Pretty

---
 src/ocamlutil/pretty.ml  | 11 ++---------
 src/ocamlutil/pretty.mli |  5 +----
 2 files changed, 3 insertions(+), 13 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 3b92aff9a..6819011f2 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -41,13 +41,6 @@
    structured text.
 *)
 
-module DLS =  Domain.DLS
-
-type 'a refDLS = 'a Domain.DLS.key
-let refDLS vl = DLS.new_key (fun () -> vl)
-let incrDLS rf = DLS.set rf (DLS.get rf + 1)
-let decrDLS rf = DLS.set rf (DLS.get rf - 1)
-
 let debug =  false
 
 let fastMode       = ref false
@@ -478,7 +471,7 @@ let rec scan ~state (abscol: int) (d: doc) : int =
 
 (** Keep a running counter of the newlines we are taking. You can read and
     reset this from user code, if you want *)
-let countNewLines = refDLS 0
+let countNewLines = Atomic.make 0
 
 (* The actual function that takes a document and prints it *)
 let emitDoc ~state
@@ -496,7 +489,7 @@ let emitDoc ~state
       [] -> failwith "Ran out of aligns"
     | x :: _ ->
 	emitString "\n" 1;
-        DLS.set countNewLines (DLS.get countNewLines + 1);
+        Atomic.incr countNewLines;
         wantIndent := true;
 	x
   in
diff --git a/src/ocamlutil/pretty.mli b/src/ocamlutil/pretty.mli
index 7857a87a8..a88d56393 100644
--- a/src/ocamlutil/pretty.mli
+++ b/src/ocamlutil/pretty.mli
@@ -52,9 +52,6 @@
 
 (** API *)
 
-(** refDLS is an alias for Domain.DLS.key *)
-type 'a refDLS = 'a Domain.DLS.key
-
 (** The type of unformated documents. Elements of this type can be 
    constructed in two ways. Either with a number of constructor shown below, 
    or using the {!Pretty.dprintf} function with a [printf]-like interface. 
@@ -315,7 +312,7 @@ val flattenBeforePrint : bool ref
 
 (** Keep a running count of the taken newlines. You can read and write this 
     from the client code if you want *)
-val countNewLines : int refDLS
+val countNewLines : int Atomic.t
 
 
 (** A function that when used at top-level in a module will direct 

From 818a00c71f2ef07206f162d6ea5f43d2e7168b18 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Jul 2025 19:08:52 +0300
Subject: [PATCH 7/8] Convert Pretty.state ref fields to mutable fields

---
 src/ocamlutil/pretty.ml | 102 ++++++++++++++++++++--------------------
 1 file changed, 51 insertions(+), 51 deletions(-)

diff --git a/src/ocamlutil/pretty.ml b/src/ocamlutil/pretty.ml
index 6819011f2..9e34b39c5 100644
--- a/src/ocamlutil/pretty.ml
+++ b/src/ocamlutil/pretty.ml
@@ -261,64 +261,64 @@ type align =
     }
 
 type state = {
-  aligns: align list ref;
+  mutable aligns: align list;
   (** The current stack of active alignment marks, with the top at the head. Never empty. *)
 
-  topAlignAbsCol: int ref;
+  mutable topAlignAbsCol: int;
   (** The absolute column of the top alignment *)
 
-  activeMarkups: int list ref;
+  mutable activeMarkups: int list;
   (** We keep a list of active markup sections. For each one we keep the column we are in *)
 
-  breaks: bool ref list ref;
+  mutable breaks: bool ref list;
   (** Keep a list of ref cells for the breaks, in the same order that we see them in the document *)
 
-  maxCol: int ref;
+  mutable maxCol: int;
   (** The maximum column that we should use *)
 
-  breakAllMode: bool ref;
+  mutable breakAllMode: bool;
   (** Sometimes we take all the optional breaks *)
 
-  alignDepth: int ref;
+  mutable alignDepth: int;
 }
 
 let create_state (): state = {
-  aligns = ref [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
-  topAlignAbsCol = ref 0;
-  activeMarkups = ref [];
-  breaks = ref [];
-  maxCol = ref 0;
-  breakAllMode = ref false;
-  alignDepth = ref 0;
+  aligns = [{ gainBreak = 0; isTaken = ref false; deltaFromPrev = ref 0; deltaToNext = ref 0; }];
+  topAlignAbsCol = 0;
+  activeMarkups = [];
+  breaks = [];
+  maxCol = 0;
+  breakAllMode = false;
+  alignDepth = 0;
 }
 
 let pushAlign ~state (abscol: int) =
-  let topalign = List.hd @@ !(state.aligns) in
+  let topalign = List.hd @@ state.aligns in
   let (res : align) =
     { gainBreak = 0; isTaken = ref false;
       deltaFromPrev = topalign.deltaToNext; (* Share with the previous *)
       deltaToNext = ref 0; (* Allocate a new ref *)} in
-  state.aligns := (res :: !(state.aligns));
-  let newdelta = abscol - !(state.topAlignAbsCol) in
+  state.aligns <- res :: state.aligns;
+  let newdelta = abscol - state.topAlignAbsCol in
   res.deltaFromPrev := newdelta;
-  state.topAlignAbsCol := abscol
+  state.topAlignAbsCol <- abscol
 
 let popAlign ~state =
-  match !(state.aligns) with
+  match state.aligns with
     top :: t when t != [] ->
-      state.aligns := t;
-      state.topAlignAbsCol := (!(state.topAlignAbsCol) - !(top.deltaFromPrev))
+      state.aligns <- t;
+      state.topAlignAbsCol <- state.topAlignAbsCol - !(top.deltaFromPrev)
   | _ -> failwith "Unmatched unalign\n"
 
 (* We are taking a newline and moving left *)
 let newline ~state =
-  let topalign = List.hd (!(state.aligns)) in (* aligns is never empty *)
+  let topalign = List.hd state.aligns in (* aligns is never empty *)
   if debug then
     dbgprintf "Taking a newline: reseting gain of %d\n" topalign.gainBreak;
   topalign.gainBreak <- 0;        (* Erase the current break info *)
-  if (!(state.breakAllMode)) && !(state.topAlignAbsCol) < !(state.maxCol) then
-    state.breakAllMode := false;
-  !(state.topAlignAbsCol)                          (* This is the new column *)
+  if state.breakAllMode && state.topAlignAbsCol < state.maxCol then
+    state.breakAllMode <- false;
+  state.topAlignAbsCol                          (* This is the new column *)
 
 
 
@@ -337,7 +337,7 @@ let chooseBestGain ~state : align option =
         end else
           loop breakingAlign resta
   in
-  loop None (!(state.aligns))
+  loop None state.aligns
 
 
 (* We have just advanced to a new column. See if we must take a line break *)
@@ -345,7 +345,7 @@ let movingRight ~state (abscol: int) : int =
   (* Keep taking the best break until we get back to the left of maxCol or no
      more are left *)
   let rec tryAgain abscol =
-    if abscol <= !(state.maxCol) then abscol else
+    if abscol <= state.maxCol then abscol else
     begin
       if debug then
         dbgprintf "Looking for a break to take in column %d\n" abscol;
@@ -353,13 +353,13 @@ let movingRight ~state (abscol: int) : int =
       match if !fastMode then None else chooseBestGain ~state with
         None -> begin
           (* No breaks are available. Take all breaks from now on *)
-          state.breakAllMode := true;
+          state.breakAllMode <- true;
           if debug then
             dbgprintf "Can't find any breaks\n";
           abscol
         end
       | Some breakingAlign -> begin
-          let topalign = List.hd (!(state.aligns)) in
+          let topalign = List.hd state.aligns in
           let theGain = breakingAlign.gainBreak in
           assert (theGain > 0);
           if debug then dbgprintf "Taking break at %d. gain=%d\n" abscol theGain;
@@ -368,7 +368,7 @@ let movingRight ~state (abscol: int) : int =
           if breakingAlign != topalign then begin
             breakingAlign.deltaToNext :=
                !(breakingAlign.deltaToNext) - theGain;
-            state.topAlignAbsCol := (!(state.topAlignAbsCol) - theGain)
+            state.topAlignAbsCol <- state.topAlignAbsCol - theGain
           end;
           tryAgain (abscol - theGain)
       end
@@ -386,17 +386,17 @@ let useAlignDepth = true
 
 (** Start an align. Return true if we have just passed the threshhold *)
 let enterAlign ~state =
-  incr state.alignDepth;
-  useAlignDepth && !(state.alignDepth) = !printDepth + 1
+  state.alignDepth <- state.alignDepth + 1;
+  useAlignDepth && state.alignDepth = !printDepth + 1
 
 (** Exit an align *)
 let exitAlign ~state =
-  decr state.alignDepth
+  state.alignDepth <- state.alignDepth - 1
 
 (** See if we are at a low-enough align level (and we should be printing
    normally) *)
 let shallowAlign ~state =
-  not useAlignDepth || !(state.alignDepth) <= !printDepth
+  not useAlignDepth || state.alignDepth <= !printDepth
 
 
 (* Pass the current absolute column and compute the new column *)
@@ -429,7 +429,7 @@ let rec scan ~state (abscol: int) (d: doc) : int =
   | Unalign -> exitAlign ~state; popAlign ~state; abscol
 
   | Line when shallowAlign ~state -> (* A forced line break *)
-      if !(state.activeMarkups) != [] then
+      if state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
       newline ~state
 
@@ -437,31 +437,31 @@ let rec scan ~state (abscol: int) (d: doc) : int =
 
   | Break when shallowAlign ~state -> (* An optional line break. Always a space
                                      followed by an optional line break *)
-      if !(state.activeMarkups) != [] then
+      if state.activeMarkups != [] then
         failwith "Line breaks inside markup sections";
       let takenref = ref false in
-      state.breaks := (takenref :: !(state.breaks));
-      let topalign = List.hd (!(state.aligns)) in (* aligns is never empty *)
-      if !(state.breakAllMode) then begin
+      state.breaks <- takenref :: state.breaks;
+      let topalign = List.hd state.aligns in (* aligns is never empty *)
+      if state.breakAllMode then begin
         takenref := true;
         newline ~state
       end else begin
         (* If there was a previous break there it stays not taken, forever.
            So we overwrite it. *)
         topalign.isTaken <- takenref;
-        topalign.gainBreak <- 1 + abscol - !(state.topAlignAbsCol);
+        topalign.gainBreak <- 1 + abscol - state.topAlignAbsCol;
         if debug then
           dbgprintf "Registering a break at %d with gain %d\n"
             (1 + abscol) topalign.gainBreak;
         movingRight ~state (1 + abscol)
       end
 
-  | Mark -> state.activeMarkups := (abscol :: !(state.activeMarkups));
+  | Mark -> state.activeMarkups <- abscol :: state.activeMarkups;
             abscol
 
   | Unmark -> begin
-      match !(state.activeMarkups) with
-        old :: rest -> state.activeMarkups := rest;
+      match state.activeMarkups with
+        old :: rest -> state.activeMarkups <- rest;
                        old
       | [] -> failwith "Too many unmark"
   end
@@ -547,10 +547,10 @@ let emitDoc ~state
     | Line when shallowAlign ~state  -> cont (newline ())
     | LeftFlush when shallowAlign ~state -> wantIndent := false;  cont (0)
     | Break when shallowAlign ~state -> begin
-        match !(state.breaks) with
+        match state.breaks with
           [] -> failwith "Break without a takenref"
         | istaken :: rest ->
-            state.breaks := rest; (* Consume the break *)
+            state.breaks <- rest; (* Consume the break *)
             if !istaken then cont (newline ())
             else begin
 	      indentIfNeeded ();
@@ -560,12 +560,12 @@ let emitDoc ~state
     end
 
     | Mark ->
-        state.activeMarkups := (abscol :: !(state.activeMarkups));
+        state.activeMarkups <- abscol :: state.activeMarkups;
         cont abscol
 
     | Unmark -> begin
-        match !(state.activeMarkups) with
-          old :: rest -> state.activeMarkups := rest;
+        match state.activeMarkups with
+          old :: rest -> state.activeMarkups <- rest;
                          cont old
         | [] -> failwith "Unmark without a mark"
     end
@@ -579,7 +579,7 @@ let emitDoc ~state
 
 let print_with_state ~width f =
   let state = create_state () in
-  state.maxCol := width;
+  state.maxCol <- width;
   f ~state
 
 (* Print a document on a channel *)
@@ -587,7 +587,7 @@ let fprint (chn: out_channel) ~(width: int) doc =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
   print_with_state ~width (fun ~state ->
       ignore (scan ~state 0 doc);
-      state.breaks := List.rev (!(state.breaks));
+      state.breaks <- List.rev state.breaks;
       emitDoc ~state (fun s nrcopies ->
           for _ = 1 to nrcopies do
             output_string chn s
@@ -600,7 +600,7 @@ let sprint ~(width : int)  doc : string =
   let doc = if !flattenBeforePrint then flatten Nil doc else doc in
   print_with_state ~width (fun ~state ->
       ignore (scan ~state 0 doc);
-      state.breaks := List.rev (!(state.breaks));
+      state.breaks <- List.rev state.breaks;
       let buf = Buffer.create 1024 in
       let rec add_n_strings str num =
         if num <= 0 then ()

From e4bf34970c80dad2810680507effee9a983f9d30 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Sun, 27 Jul 2025 11:42:22 +0300
Subject: [PATCH 8/8] Remove domain_shims dependency again

---
 dune-project     | 1 -
 goblint-cil.opam | 1 -
 src/dune         | 2 +-
 test/Makefile    | 2 +-
 4 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/dune-project b/dune-project
index 6932d5aaa..424a6c1b6 100644
--- a/dune-project
+++ b/dune-project
@@ -35,7 +35,6 @@ This is a fork of the 'cil' package used for 'goblint'. Major changes include:
     conf-perl
     cppo
     conf-gcc
-    domain_shims
   )
   (conflicts cil) ; only because we both install the cilly executable
 )
diff --git a/goblint-cil.opam b/goblint-cil.opam
index d66c62b82..0a31ec7e0 100644
--- a/goblint-cil.opam
+++ b/goblint-cil.opam
@@ -42,7 +42,6 @@ depends: [
   "conf-perl"
   "cppo"
   "conf-gcc"
-  "domain_shims"
 ]
 conflicts: ["cil"]
 build: [
diff --git a/src/dune b/src/dune
index a804b0a1b..ef8e36031 100644
--- a/src/dune
+++ b/src/dune
@@ -3,7 +3,7 @@
 (library
   (public_name goblint-cil)
   (name goblintCil)
-  (libraries zarith unix str stdlib-shims domain_shims)
+  (libraries zarith unix str stdlib-shims)
   (modules (:standard \ main mainFeature ciloptions machdepConfigure machdepArchConfigure modelConfigure))
 )
 
diff --git a/test/Makefile b/test/Makefile
index 3463c0f77..189d391b8 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -276,7 +276,7 @@ else
 endif
 
 testrun/% : $(SMALL1)/%.ml
-	ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith -package domain_shims unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) threads.$(CMXA) domain_shims.$(CMXA) -thread \
+	ocamlfind $(CAMLC) -I $(OBJDIR_DUNE) -I $(OBJDIR_MAKE) -package zarith unix.$(CMXA) str.$(CMXA) zarith.$(CMXA) \
                  goblintCil.$(CMXA) \
                  $(EXEOUT) $(basename $<).exe $<
 	$(basename $<).exe