summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
authorSon Ho2022-02-02 17:06:40 +0100
committerSon Ho2022-02-02 17:06:40 +0100
commit412d7215517f42c90ba6f53432798a5eef093475 (patch)
tree5a696c64bbbe3846afb212f00d229cc8eab85cc3 /src
parentee797b755311d397744bbe008ffb4be5180530e4 (diff)
Work on formatting
Diffstat (limited to 'src')
-rw-r--r--src/ExtractToFStar.ml12
1 files changed, 7 insertions, 5 deletions
diff --git a/src/ExtractToFStar.ml b/src/ExtractToFStar.ml
index f4cc0d6c..340092b4 100644
--- a/src/ExtractToFStar.ml
+++ b/src/ExtractToFStar.ml
@@ -205,7 +205,8 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
*
* Or if there isn't enough space on one line:
* ```
- * type t = {
+ * type t =
+ * {
* x : int;
* y : bool;
* }
@@ -222,7 +223,6 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
F.pp_print_space fmt ();
F.pp_print_string fmt "{";
(* The body itself *)
- F.pp_open_hvbox fmt 0;
F.pp_open_hvbox fmt ctx.indent_incr;
F.pp_print_space fmt ();
(* Print the fields *)
@@ -242,8 +242,8 @@ let extract_type_def_struct_body (ctx : extraction_ctx) (fmt : F.formatter)
List.iter (fun (fid, f) -> print_field fid f) fields;
(* Close *)
F.pp_close_box fmt ();
- F.pp_print_string fmt "}";
- F.pp_close_box fmt ())
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "}")
let extract_type_def_enum_body (ctx : extraction_ctx) (fmt : F.formatter)
(def : type_def) (def_name : string) (type_params : string list)
@@ -408,7 +408,9 @@ let extract_type_def (ctx : extraction_ctx) (fmt : F.formatter) (def : type_def)
F.pp_print_string fmt pname;
F.pp_print_space fmt ())
def.type_params;
- F.pp_print_string fmt " : Type0)");
+ F.pp_print_string fmt ":";
+ F.pp_print_space fmt ();
+ F.pp_print_string fmt "Type0)");
(* Print the "=" *)
F.pp_print_space fmt ();
F.pp_print_string fmt "=";