diff options
author | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-05 02:12:36 +0100 |
---|---|---|
committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-02-07 22:56:56 +0100 |
commit | df14dac0e6e9d9819dcc3b1601e150af7c142597 (patch) | |
tree | b2cd633c679810d0eae8a9441b11ac2f9902c1a8 /plugins/extraction | |
parent | 093ce7c6a03e6e48c9b8f20a810d553fb953fe72 (diff) |
Extraction cosmetic: no whitespaces in printing empty modules
Diffstat (limited to 'plugins/extraction')
-rw-r--r-- | plugins/extraction/ocaml.ml | 12 |
1 files changed, 8 insertions, 4 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 404939cff..d89bf95ee 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -625,8 +625,10 @@ and pp_module_type params = function let l = List.rev l in pop_visible (); str "sig" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" | MTwith(mt,ML_With_type(idl,vl,typ)) -> let ids = pp_parameters (rename_tvars keywords vl) in let mp_mt = msid_of_mt mt in @@ -701,8 +703,10 @@ and pp_module_expr params = function let l = List.rev l in pop_visible (); str "struct" ++ fnl () ++ - v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ - fnl () ++ str "end" + (if List.is_empty l then mt () + else + v 1 (str " " ++ prlist_with_sep cut2 identity l) ++ fnl ()) + ++ str "end" let rec prlist_sep_nonempty sep f = function | [] -> mt () |