aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/extraction
diff options
context:
space:
mode:
authorGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-02-05 02:12:36 +0100
committerGravatar Pierre Letouzey <pierre.letouzey@inria.fr>2017-02-07 22:56:56 +0100
commitdf14dac0e6e9d9819dcc3b1601e150af7c142597 (patch)
treeb2cd633c679810d0eae8a9441b11ac2f9902c1a8 /plugins/extraction
parent093ce7c6a03e6e48c9b8f20a810d553fb953fe72 (diff)
Extraction cosmetic: no whitespaces in printing empty modules
Diffstat (limited to 'plugins/extraction')
-rw-r--r--plugins/extraction/ocaml.ml12
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 ()