don't forget to mark degrouted in convex grout case

hazelgrove · Oct 27, 2024 · 5f26290 · 5f26290
1 parent b7eb795
commit 5f26290
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 2 deletions.
diff --git a/src/core/parser/Grouter.re b/src/core/parser/Grouter.re
@@ -121,13 +121,19 @@ let rec degrout = (c: Cell.t): Cells.t =>
       | [hd, ...tl] when Cell.Space.is_space(l) =>
         let l = Cell.mark_degrouted(l, ~side=R);
         [Cell.pad(~squash=false, ~l, hd), ...tl];
+      | [] when Cell.Space.is_space(l) =>
+        let l = Cell.mark_degrouted(l, ~side=R);
+        [l];
       | _ => [l, ...cells]
       };
     let cells_lr =
       switch (Lists.Framed.ft(cells_l)) {
       | Some((pre, ft)) when Cell.Space.is_space(r) =>
         let r = Cell.mark_degrouted(~side=L, r);
         Lists.Framed.put_ft(pre, Cell.pad(~squash=false, ft, ~r));
+      | None when Cell.Space.is_space(r) =>
+        let r = Cell.mark_degrouted(~side=L, r);
+        [r];
       | _ => cells_l @ [r]
       };
     List.concat_map(degrout, cells_lr);

diff --git a/src/core/structure/marks/Marks.re b/src/core/structure/marks/Marks.re
@@ -52,9 +52,13 @@ module Cell = {
   let pp = (out, {cursor, obligs, dirty, degrouted} as marks) =>
     if (is_empty(marks)) {
       Fmt.nop(out, marks);
-    } else if (Option.is_none(cursor) && Path.Map.is_empty(dirty)) {
+    } else if (Option.is_none(cursor)
+               && Path.Map.is_empty(dirty)
+               && !degrouted) {
       Fmt.pf(out, "obligs: %a", Path.Map.pp(Mtrl.T.pp), obligs);
-    } else if (Path.Map.is_empty(obligs) && Path.Map.is_empty(dirty)) {
+    } else if (Path.Map.is_empty(obligs)
+               && Path.Map.is_empty(dirty)
+               && !degrouted) {
       Fmt.pf(out, "cursor: %a", Path.Cursor.pp, Option.get(cursor));
     } else {
       Fmt.pf(