improved line breaks a bit

src/sail_lean_backend/pretty_print_lean.ml

@@ -274,10 +274,10 @@ let string_of_exp_con (E_aux (e, _)) =
   | E_let _ -> "E_let"
 
 let wrap_with_pure (needs_return : bool) (d : document) =
-  if needs_return then parens (nest 2 (flow (break 1) [string "pure"; d])) else d
+  if needs_return then parens (nest 2 (flow space [string "pure"; d])) else d
 
 let wrap_with_left_arrow (needs_return : bool) (d : document) =
-  if needs_return then parens (nest 2 (flow (break 1) [string "←"; d])) else d
+  if needs_return then parens (nest 2 (flow space [string "←"; d])) else d
 
 let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
   let env = env_of_tannot annot in
@@ -327,7 +327,7 @@ let rec doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
   | E_internal_return e -> doc_exp false ctx e (* ??? *)
   | E_struct fexps ->
       let args = List.map d_of_field fexps in
-      wrap_with_pure as_monadic (braces (space ^^ nest 2 (separate hardline args) ^^ space))
+      wrap_with_pure as_monadic (braces (space ^^ align (separate hardline args) ^^ space))
   | E_field (exp, id) ->
       (* TODO *)
       wrap_with_pure as_monadic (doc_exp false ctx exp ^^ dot ^^ doc_id_ctor id)

test/lean/struct.expected.lean

@@ -7,9 +7,8 @@ structure My_struct where
   field2 : (BitVec 1)
 
 def undefined_My_struct (lit : Unit) : SailM My_struct := do
-  (pure
-    { field1 := (← sorry)
-      field2 := (← sorry) })
+  (pure { field1 := (← sorry)
+          field2 := (← sorry) })
 
 def struct_field2 (s : My_struct) : (BitVec 1) :=
   s.field2