From 8c5adfd5acb883a3bc2850b6fc8c29d352a421f8 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 17:52:39 +0200 Subject: [pp] Remove unused printing tagging infrastructure. Applications of it were not clear/unproven, it made printers more complex (as they needed to be functors) and as it lacked examples it confused some people. The printers now tag unconditionally, it is up to the backends to interpreted the tags. Tagging (and indeed the notion of rich document) should be reworked in a follow-up patch, so they are in sync, but this is a first step. Tested, test-suite passes. Notes: - We remove the `Richprinter` module. It was only used in the `annotate` IDE protocol call, its output was identical to the normal printer (or even inconsistent if taggers were not kept manually in sync). - Note that Richpp didn't need a single change. In particular, its main API entry point `Richpp.rich_pp` is not used by anyone. --- plugins/ltac/pptactic.ml | 101 ++++++++++++------------------------------- plugins/ltac/pptactic.mli | 70 ++++++++++++++++++++++++++---- plugins/ltac/pptacticsig.mli | 81 ---------------------------------- 3 files changed, 89 insertions(+), 163 deletions(-) delete mode 100644 plugins/ltac/pptacticsig.mli (limited to 'plugins') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6f4ef37b44..9dacce28d5 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -27,6 +27,33 @@ open Pputils open Ppconstr open Printer +module Tag = +struct + let keyword = + let style = Terminal.make ~bold:true () in + Ppstyle.make ~style ["tactic"; "keyword"] + + let primitive = + let style = Terminal.make ~fg_color:`LIGHT_GREEN () in + Ppstyle.make ~style ["tactic"; "primitive"] + + let string = + let style = Terminal.make ~fg_color:`LIGHT_RED () in + Ppstyle.make ~style ["tactic"; "string"] + +end + +let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s +let do_not_tag _ x = x +let tag_keyword = tag Tag.keyword +let tag_primitive = tag Tag.primitive +let tag_string = tag Tag.string +let tag_glob_tactic_expr = do_not_tag +let tag_glob_atomic_tactic_expr = do_not_tag +let tag_raw_tactic_expr = do_not_tag +let tag_raw_atomic_tactic_expr = do_not_tag +let tag_atomic_tactic_expr = do_not_tag + let pr_global x = Nametab.pr_global_env Id.Set.empty x type 'a grammar_tactic_prod_item_expr = @@ -64,30 +91,6 @@ type 'a extra_genarg_printer = (tolerability -> Val.t -> std_ppcmds) -> 'a -> std_ppcmds -module Make - (Ppconstr : Ppconstrsig.Pp) - (Taggers : sig - val tag_keyword - : std_ppcmds -> std_ppcmds - val tag_primitive - : std_ppcmds -> std_ppcmds - val tag_string - : std_ppcmds -> std_ppcmds - val tag_glob_tactic_expr - : glob_tactic_expr -> std_ppcmds -> std_ppcmds - val tag_glob_atomic_tactic_expr - : glob_atomic_tactic_expr -> std_ppcmds -> std_ppcmds - val tag_raw_tactic_expr - : raw_tactic_expr -> std_ppcmds -> std_ppcmds - val tag_raw_atomic_tactic_expr - : raw_atomic_tactic_expr -> std_ppcmds -> std_ppcmds - val tag_atomic_tactic_expr - : atomic_tactic_expr -> std_ppcmds -> std_ppcmds - end) -= struct - - open Taggers - let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -1206,37 +1209,6 @@ module Make let pr_atomic_tactic env = pr_atomic_tactic_level env ltop -end - -module Tag = -struct - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["tactic"; "keyword"] - - let primitive = - let style = Terminal.make ~fg_color:`LIGHT_GREEN () in - Ppstyle.make ~style ["tactic"; "primitive"] - - let string = - let style = Terminal.make ~fg_color:`LIGHT_RED () in - Ppstyle.make ~style ["tactic"; "string"] - -end - -include Make (Ppconstr) (struct - let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s - let do_not_tag _ x = x - let tag_keyword = tag Tag.keyword - let tag_primitive = tag Tag.primitive - let tag_string = tag Tag.string - let tag_glob_tactic_expr = do_not_tag - let tag_glob_atomic_tactic_expr = do_not_tag - let tag_raw_tactic_expr = do_not_tag - let tag_raw_atomic_tactic_expr = do_not_tag - let tag_atomic_tactic_expr = do_not_tag -end) - let declare_extra_genarg_pprule wit (f : 'a raw_extra_genarg_printer) (g : 'b glob_extra_genarg_printer) @@ -1338,22 +1310,3 @@ let () = let pr_unit _ _ _ () = str "()" in let printer _ _ prtac = prtac (0, E) in declare_extra_genarg_pprule wit_ltac printer printer pr_unit - -module Richpp = struct - - include Make (Ppconstr.Richpp) (struct - open Ppannotation - open Genarg - let do_not_tag _ x = x - let tag e s = Pp.tag (Pp.Tag.inj e tag) s - let tag_keyword = tag AKeyword - let tag_primitive = tag AKeyword - let tag_string = do_not_tag () - let tag_glob_tactic_expr e = tag (AGlbGenArg (in_gen (glbwit wit_ltac) e)) - let tag_glob_atomic_tactic_expr = do_not_tag - let tag_raw_tactic_expr e = tag (ARawGenArg (in_gen (rawwit wit_ltac) e)) - let tag_raw_atomic_tactic_expr = do_not_tag - let tag_atomic_tactic_expr = do_not_tag - end) - -end diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 86e3ea5484..43e22dba3f 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -13,6 +13,8 @@ open Pp open Genarg open Geninterp open Names +open Misctypes +open Environ open Constrexpr open Tacexpr open Ppextend @@ -54,14 +56,66 @@ type pp_tactic = { val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit -(** The default pretty-printers produce {!Pp.std_ppcmds} that are - interpreted as raw strings. *) -include Pptacticsig.Pp +val pr_with_occurrences : + ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds +val pr_red_expr : + ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds +val pr_may_eval : + ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds + +val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds +val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds + +val pr_in_clause : + ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + +val pr_clauses : bool option -> + ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + +val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds + +val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds + +val pr_raw_extend: env -> int -> + ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds + +val pr_glob_extend: env -> int -> + ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds + +val pr_extend : + (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + +val pr_alias_key : Names.KerName.t -> std_ppcmds + +val pr_alias : (Val.t -> std_ppcmds) -> + int -> Names.KerName.t -> Val.t list -> std_ppcmds + +val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds + +val pr_raw_tactic : raw_tactic_expr -> std_ppcmds + +val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds + +val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds + +val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds + +val pr_hintbases : string list option -> std_ppcmds + +val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds + +val pr_bindings : + ('constr -> std_ppcmds) -> + ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds + +val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds + +val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> + ('b, 'a) match_rule -> std_ppcmds + +val pr_value : tolerability -> Val.t -> std_ppcmds -(** The rich pretty-printers produce {!Pp.std_ppcmds} that are - interpreted as annotated strings. The annotations can be - retrieved using {!RichPp.rich_pp}. Their definitions are - located in {!Ppannotation.t}. *) -module Richpp : Pptacticsig.Pp val ltop : tolerability diff --git a/plugins/ltac/pptacticsig.mli b/plugins/ltac/pptacticsig.mli deleted file mode 100644 index 74ddd377ad..0000000000 --- a/plugins/ltac/pptacticsig.mli +++ /dev/null @@ -1,81 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds - val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds - val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds - - val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds - - val pr_in_clause : - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds - - val pr_clauses : bool option -> - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds - - val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds - - val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds - - val pr_raw_extend: env -> int -> - ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds - - val pr_glob_extend: env -> int -> - ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds - - val pr_extend : - (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds - - val pr_alias_key : Names.KerName.t -> std_ppcmds - - val pr_alias : (Val.t -> std_ppcmds) -> - int -> Names.KerName.t -> Val.t list -> std_ppcmds - - val pr_alias_key : Names.KerName.t -> std_ppcmds - - val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds - - val pr_raw_tactic : raw_tactic_expr -> std_ppcmds - - val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds - - val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds - - val pr_atomic_tactic : env -> atomic_tactic_expr -> std_ppcmds - - val pr_hintbases : string list option -> std_ppcmds - - val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds - - val pr_bindings : - ('constr -> std_ppcmds) -> - ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds - - val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds - - val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('b, 'a) match_rule -> std_ppcmds - - val pr_value : tolerability -> Val.t -> std_ppcmds - -end -- cgit v1.2.3 From 14155762a7cd46ed6a3e9cf2a58e11ee1244b188 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 Jun 2016 18:31:05 +0200 Subject: [pp] Replace `Pp.Tag` by `Ppstyle.tag` = `string list` This is what has always been used, so it doesn't represent a functional change. This is just a preliminary patch, but many more possibilities could be done wrt tags. --- plugins/ltac/pptactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 9dacce28d5..d9410a0885 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -43,7 +43,7 @@ struct end -let tag t s = Pp.tag (Pp.Tag.inj t Ppstyle.tag) s +let tag t s = Pp.tag t s let do_not_tag _ x = x let tag_keyword = tag Tag.keyword let tag_primitive = tag Tag.primitive -- cgit v1.2.3 From 2617a83e572531e26734cff8b9eb8aa09d49b850 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 27 Sep 2016 16:33:47 +0200 Subject: [pp] Remove `Pp.stras`. Mostly unused, we ought to limit spacing in the boxes themselves. --- plugins/extraction/common.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 0a591e786f..fc8d5356c8 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -67,7 +67,9 @@ let pp_boxed_tuple f = function blocks is less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) -let fnl () = stras (1000000,"") ++ fnl () +(* EG: This looks quite suspicious... but beware of bugs *) +(* let fnl () = stras (1000000,"") ++ fnl () *) +let fnl () = fnl () let fnl2 () = fnl () ++ fnl () -- cgit v1.2.3 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') diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index d89bf95ee8..d8e3821557 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 From fd6271089a0f0fcaa6d89e347d76247c7c831d23 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 30 Sep 2016 19:44:13 +0200 Subject: [pp] Force well-formed boxes by construction. We replace open/close box commands in favor of the create box ones. --- plugins/rtauto/proof_search.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml index 8b92611136..1ad4d622b2 100644 --- a/plugins/rtauto/proof_search.ml +++ b/plugins/rtauto/proof_search.ml @@ -505,12 +505,12 @@ let pp_mapint map = pp_form obj ++ str " => " ++ pp_list (fun (i,f) -> pp_form f) l ++ cut ()) ) map; - str "{ " ++ vb 0 ++ (!pp) ++ str " }" ++ close () + str "{ " ++ hv 0 (!pp ++ str " }") let pp_connect (i,j,f1,f2) = pp_form f1 ++ str " => " ++ pp_form f2 let pp_gl gl= cut () ++ - str "{ " ++ vb 0 ++ + str "{ " ++ hv 0 ( begin match gl.abs with None -> str "" @@ -520,7 +520,7 @@ let pp_gl gl= cut () ++ str "norev =" ++ pp_intmap gl.norev_hyps ++ cut () ++ str "arrows=" ++ pp_mapint gl.right ++ cut () ++ str "cnx =" ++ pp_list pp_connect gl.cnx ++ cut () ++ - str "goal =" ++ pp_form gl.gl ++ str " }" ++ close () + str "goal =" ++ pp_form gl.gl ++ str " }") let pp = function -- cgit v1.2.3 From 5b8bfee9d80e550cd81e326ec134430b2a4797a5 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 29 Sep 2016 16:30:21 +0200 Subject: [pp] Make feedback the only logging mechanism. Previously to this patch, Coq featured to distinct logging paths: the console legacy one, based on `Pp.std_ppcmds` and Ocaml's `Format` module, and the `Feedback` one, intended to encapsulate message inside a more general, GUI-based feedback protocol. This patch removes the legacy logging path and makes feedback canonical. Thus, the core of Coq has no dependency on console code anymore. Additionally, this patch resolves the duplication of "document" formats present in the same situation. The original console-based printing code relied on an opaque datatype `std_ppcmds`, (mostly a reification of `Format`'s format strings) that could be then rendered to the console. However, the feedback path couldn't reuse this type due to its opaque nature. The first versions just embedded rending of `std_ppcmds` to a string, however in 8.5 a new "rich printing" type, `Richpp.richpp` was introduced. The idea for this type was to be serializable, however it brought several problems: it didn't have proper document manipulation operations, its format was overly verbose and didn't preserve the full layout, and it still relied on `Format` for generation, making client-side rendering difficult. We thus follow the plan outlined in CEP#9, that is to say, we take a public and refactored version of `std_ppcmds` as the canonical "document type", and move feedback to be over there. The toplevel now is implemented as a feedback listener and has ownership of the console. `richpp` is now IDE-specific, and only used for legacy rendering. It could go away in future versions. `std_ppcmds` carries strictly more information and is friendlier to client-side rendering and display control. Thus, the new panorama is: - `Feedback` has become a very module for event dispatching. - `Pp` contains a target-independent box-based document format. It also contains the `Format`-based renderer. - All console access lives in `toplevel`, with console handlers private to coqtop. _NOTE_: After this patch, many printing parameters such as printing width or depth should be set client-side. This works better IMO, clients don't need to notify Coq about resizing anywmore. Indeed, for box-based capable backends such as HTML or LaTeX, the UI can directly render and let the engine perform the word breaking work. _NOTE_: Many messages could benefit from new features of the output format, however we have chosen not to alter them to preserve output. A Future commits will move console tag handling in `Pp_style` to `toplevel/`, where it logically belongs. The only change with regards to printing is that the "Error:" header was added to console output in several different positions, we have removed some of this duplication, now error messages should be a bit more consistent. --- plugins/extraction/extract_env.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'plugins') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index e019bb3c2a..ee623c5ca0 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -472,13 +472,14 @@ let formatter dry file = if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) else match file with - | Some f -> Pp_control.with_output_to f + | Some f -> Topfmt.with_output_to f | None -> Format.formatter_of_buffer buf in + (* XXX: Fixme, this shouldn't depend on Topfmt *) (* We never want to see ellipsis ... in extracted code *) Format.pp_set_max_boxes ft max_int; (* We reuse the width information given via "Set Printing Width" *) - (match Pp_control.get_margin () with + (match Topfmt.get_margin () with | None -> () | Some i -> Format.pp_set_margin ft i; -- cgit v1.2.3 From 3fc02bb2034a648c9c27b76a9e7b4e02a78e55b9 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 5 Dec 2016 17:56:22 +0100 Subject: [pp] Move terminal-specific tagging to the toplevel. Previously, tags were associated to terminal styles, which doesn't make sense on terminal-free pretty printing scenarios. This commit moves tag interpretation to the toplevel terminal handling module `Topfmt`. --- plugins/ltac/pptactic.ml | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) (limited to 'plugins') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d9410a0885..dc418d530e 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -29,17 +29,10 @@ open Printer module Tag = struct - let keyword = - let style = Terminal.make ~bold:true () in - Ppstyle.make ~style ["tactic"; "keyword"] - let primitive = - let style = Terminal.make ~fg_color:`LIGHT_GREEN () in - Ppstyle.make ~style ["tactic"; "primitive"] - - let string = - let style = Terminal.make ~fg_color:`LIGHT_RED () in - Ppstyle.make ~style ["tactic"; "string"] + let keyword = "tactic.keyword" + let primitive = "tactic.primitive" + let string = "tactic.string" end -- cgit v1.2.3 From 00b1ceb18db39334a357784a114e45a9012cf594 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 6 Feb 2017 04:52:43 +0100 Subject: [extraction] Flush formatters at end of output. Previous implementations of `Pp` flushed on newline, however, depending on the formatter this may not be always the case. We now alwayas flush the formatters before closing the file as this is the intended behavior. --- plugins/extraction/extract_env.ml | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'plugins') diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index ee623c5ca0..2b12462ad5 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -519,8 +519,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Impl; pp_with ft (d.preamble mo comment opened unsafe_needs); pp_with ft (d.pp_struct struc); + Format.pp_print_flush ft (); Option.iter close_out cout; with reraise -> + Format.pp_print_flush ft (); Option.iter close_out cout; raise reraise end; if not dry then Option.iter info_file fn; @@ -533,8 +535,10 @@ let print_structure_to_file (fn,si,mo) dry struc = set_phase Intf; pp_with ft (d.sig_preamble mo comment opened unsafe_needs); pp_with ft (d.pp_sig (signature_of_structure struc)); + Format.pp_print_flush ft (); close_out cout; with reraise -> + Format.pp_print_flush ft (); close_out cout; raise reraise end; info_file si) -- cgit v1.2.3