summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-02-10 10:05:42 +0100
committerSon Ho2022-02-10 10:05:42 +0100
commitdcff2372f056af24c176b90797c10412b8b5f893 (patch)
treef1444b2272aa2caa7d9581f55d2cc1b2c23bd38a
parent1c7c1bb9fac25dda0fb0412b33227299ccfdd3f0 (diff)
Slightly improve formatting
-rw-r--r--src/ExtractToFStar.ml10
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