From e660a4d575ba55bd23c64b5bd7b4e435be82d7ed Mon Sep 17 00:00:00 2001
From: Aymeric Fromherz
Date: Thu, 23 May 2024 10:58:47 +0200
Subject: Improve formatting of Lean struct projectors

---
 compiler/ExtractTypes.ml | 8 ++++++--
 1 file changed, 6 insertions(+), 2 deletions(-)

diff --git a/compiler/ExtractTypes.ml b/compiler/ExtractTypes.ml
index 4272e7a9..8520b0fb 100644
--- a/compiler/ExtractTypes.ml
+++ b/compiler/ExtractTypes.ml
@@ -1696,8 +1696,11 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
 
         let extract_field_proj (field_id : FieldId.id) (_ : field) : unit =
           F.pp_print_space fmt ();
-          (* Box for the projector definition *)
+          (* Outer box for the projector definition *)
           F.pp_open_hvbox fmt 0;
+          (* Inner box for the projector definition *)
+          F.pp_open_hvbox fmt ctx.indent_incr;
+
           (* Box for the [def ADT.proj ... :=] *)
           F.pp_open_hovbox fmt ctx.indent_incr;
           F.pp_print_string fmt "def";
@@ -1775,7 +1778,8 @@ let extract_type_decl_lean_record_field_projectors (ctx : extraction_ctx)
           (* Close the box for the whole match *)
           F.pp_close_box fmt ();
 
-          (* Close the box for projector definition *)
+          F.pp_close_box fmt ();
+          (* Close the outer box for projector definition *)
           F.pp_close_box fmt ();
           (* Add breaks to insert new lines between definitions *)
           F.pp_print_break fmt 0 0
-- 
cgit v1.2.3