diff options
author | Son Ho | 2022-02-10 10:05:42 +0100 |
---|---|---|
committer | Son Ho | 2022-02-10 10:05:42 +0100 |
commit | dcff2372f056af24c176b90797c10412b8b5f893 (patch) | |
tree | f1444b2272aa2caa7d9581f55d2cc1b2c23bd38a | |
parent | 1c7c1bb9fac25dda0fb0412b33227299ccfdd3f0 (diff) |
Slightly improve formatting
-rw-r--r-- | src/ExtractToFStar.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml index 506a6d04..def63db7 100644 --- a/src/ExtractToFStar.ml +++ b/src/ExtractToFStar.ml @@ -957,6 +957,8 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) (* The type parameters *) if def.signature.type_params <> [] then ( F.pp_print_space fmt (); + (* Open a box for the type parameters *) + F.pp_open_hovbox fmt 0; F.pp_print_string fmt "("; List.iter (fun (p : type_var) -> @@ -966,12 +968,16 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) def.signature.type_params; F.pp_print_string fmt ":"; F.pp_print_space fmt (); - F.pp_print_string fmt "Type0)"); + F.pp_print_string fmt "Type0)"; + (* Close the box for the type parameters *) + F.pp_close_box fmt ()); (* The input parameters - note that doing this adds bindings to the context *) let ctx_body = List.fold_left (fun ctx (lv : typed_lvalue) -> F.pp_print_space fmt (); + (* Open a box for the input parameter *) + F.pp_open_hovbox fmt 0; F.pp_print_string fmt "("; let ctx = extract_typed_lvalue ctx fmt false lv in F.pp_print_space fmt (); @@ -979,6 +985,8 @@ let extract_fun_parameters (ctx : extraction_ctx) (fmt : F.formatter) F.pp_print_space fmt (); extract_ty ctx fmt false lv.ty; F.pp_print_string fmt ")"; + (* Close the box for the input parameters *) + F.pp_close_box fmt (); ctx) ctx def.inputs_lvs in |