From dcff2372f056af24c176b90797c10412b8b5f893 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Thu, 10 Feb 2022 10:05:42 +0100 Subject: Slightly improve formatting --- src/ExtractToFStar.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) (limited to 'src') 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 -- cgit v1.2.3