From 8f8af9e4ebf1ea1ed15f765196ef5af8a77d3c27 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:06:43 +0200 Subject: [pp] Prepare for serialization, remove opaque glue. We also remove flushing operations `msg_with`, now the flushing responsibility belong to the owner of the formatter. --- plugins/extraction/ocaml.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/extraction/ocaml.ml') 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 = -- cgit v1.2.3