diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 14:09:41 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 14:09:41 +0100 |
commit | 6e0ca299c407125a8d65f54ab424bdae3667125e (patch) | |
tree | 2f968c31b85b22190d4ce9f2472f4cb6cd0a6ad9 /plugins/extraction/ocaml.ml | |
parent | 051ef20a9f9c496fc6a5143de97450ccf7786c5b (diff) | |
parent | aa9e94275ccac92311a6bdac563b61a6c7876cec (diff) |
Merge PR#390: Updates to the Pretty Printing Infrastructure
Diffstat (limited to 'plugins/extraction/ocaml.ml')
-rw-r--r-- | plugins/extraction/ocaml.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d89bf95ee..d8e382155 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -66,7 +66,7 @@ let pp_header_comment = function | None -> mt () | Some com -> pp_comment com ++ fnl2 () -let then_nl pp = if Pp.is_empty pp then mt () else pp ++ fnl () +let then_nl pp = if Pp.ismt pp then mt () else pp ++ fnl () let pp_tdummy usf = if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl () else mt () @@ -618,7 +618,7 @@ and pp_module_type params = function push_visible mp params; let try_pp_specif l x = let px = pp_specif x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_specif *) let l = List.fold_left try_pp_specif [] sign in @@ -696,7 +696,7 @@ and pp_module_expr params = function push_visible mp params; let try_pp_structure_elem l x = let px = pp_structure_elem x in - if Pp.is_empty px then l else px::l + if Pp.ismt px then l else px::l in (* We cannot use fold_right here due to side effects in pp_structure_elem *) let l = List.fold_left try_pp_structure_elem [] sel in @@ -714,7 +714,7 @@ let rec prlist_sep_nonempty sep f = function | h::t -> let e = f h in let r = prlist_sep_nonempty sep f t in - if Pp.is_empty e then r + if Pp.ismt e then r else e ++ sep () ++ r let do_struct f s = |