diff options
| -rw-r--r-- | src/ExtractToFStar.ml | 9 | ||||
| -rw-r--r-- | src/Translate.ml | 3 |
2 files changed, 8 insertions, 4 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 340092b4..6fd141cc 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -222,9 +222,9 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter) else ( F.pp_print_space fmt (); F.pp_print_string fmt "{"; + F.pp_print_break fmt 1 ctx.indent_incr; (* The body itself *) - F.pp_open_hvbox fmt ctx.indent_incr; - F.pp_print_space fmt (); + F.pp_open_hvbox fmt 0; (* Print the fields *) let print_field (field_id : FieldId.id) (f : field) : unit = let field_name = ctx_get_field def.def_id field_id ctx in @@ -235,11 +235,12 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_ty ctx fmt false f.field_ty; F.pp_print_string fmt ";"; - F.pp_print_space fmt (); F.pp_close_box fmt () in let fields = FieldId.mapi (fun fid f -> (fid, f)) fields in - List.iter (fun (fid, f) -> print_field fid f) fields; + Collections.List.iter_link (F.pp_print_space fmt) + (fun (fid, f) -> print_field fid f) + fields; (* Close *) F.pp_close_box fmt (); F.pp_print_space fmt (); diff --git a/src/Translate.ml b/src/Translate.ml index 874d852e..75975704 100644 --- a/src/Translate.ml +++ b/src/Translate.ml @@ -322,6 +322,9 @@ let translate_module (filename : string) (config : C.partial_config) trans_funs) in + (* Set the margin *) + Format.pp_set_margin fmt 80; + (* Create a vertical box *) Format.pp_open_vbox fmt 0; |