diff --git a/infer/src/backend/ondemand.ml b/infer/src/backend/ondemand.ml index d8014751e..a13ec0da2 100644 --- a/infer/src/backend/ondemand.ml +++ b/infer/src/backend/ondemand.ml @@ -87,7 +87,7 @@ let save_global_state () = (* use a new global counter for the callee *) { abs_val= !BiabductionConfig.abs_val ; abstraction_rules= Abs.get_current_rules () - ; delayed_prints= L.get_delayed_prints () + ; delayed_prints= L.get_and_reset_delayed_prints () ; footprint_mode= !BiabductionConfig.footprint ; html_formatter= !Printer.curr_html_formatter ; name_generator= Ident.NameGenerator.get_current () diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 5ec68d6a0..8072fe129 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -165,11 +165,10 @@ end (** Execute the delayed print actions *) let force_delayed_prints () = - F.fprintf !curr_html_formatter "@?" ; + F.pp_print_flush !curr_html_formatter () ; (* flush html stream *) - L.force_delayed_prints !curr_html_formatter (L.get_delayed_prints ()) ; - F.fprintf !curr_html_formatter "@?" ; - L.reset_delayed_prints () + L.force_and_reset_delayed_prints !curr_html_formatter ; + F.pp_print_flush !curr_html_formatter () (** Start a session, and create a new html file for the node if it does not exist yet *) diff --git a/infer/src/base/Logging.ml b/infer/src/base/Logging.ml index 14588e60b..4fe94f451 100644 --- a/infer/src/base/Logging.ml +++ b/infer/src/base/Logging.ml @@ -400,8 +400,13 @@ let force_delayed_print fmt = function else pp Pp.text fmt x -let force_delayed_prints fmt rev_delayed_prints = - rev_delayed_prints |> List.rev |> List.iter ~f:(force_delayed_print fmt) +(** reset the delayed print actions *) +let reset_delayed_prints () = delayed_actions := [] + +(** return the delayed print actions *) +let get_and_reset_delayed_prints () = + let res = !delayed_actions in + reset_delayed_prints () ; res (** extend the current print log *) @@ -415,11 +420,9 @@ let d_pp pp x = add_print_action (PT_generic (pp, x)) let d_pp_with_pe ?color pp x = add_print_action (PT_generic_with_pe (color, pp, x)) -(** reset the delayed print actions *) -let reset_delayed_prints () = delayed_actions := [] +let force_and_reset_delayed_prints fmt = + get_and_reset_delayed_prints () |> List.rev |> List.iter ~f:(force_delayed_print fmt) -(** return the delayed print actions *) -let get_delayed_prints () = !delayed_actions (** set the delayed print actions *) let set_delayed_prints new_delayed_actions = delayed_actions := new_delayed_actions diff --git a/infer/src/base/Logging.mli b/infer/src/base/Logging.mli index c1c35cae1..8de7d47c4 100644 --- a/infer/src/base/Logging.mli +++ b/infer/src/base/Logging.mli @@ -88,10 +88,10 @@ val d_pp : (F.formatter -> 'a -> unit) -> 'a -> unit val d_pp_with_pe : ?color:Pp.color -> (Pp.env -> F.formatter -> 'a -> unit) -> 'a -> unit -val force_delayed_prints : F.formatter -> delayed_prints -> unit +val force_and_reset_delayed_prints : F.formatter -> unit -val get_delayed_prints : unit -> delayed_prints -(** return the delayed print actions *) +val get_and_reset_delayed_prints : unit -> delayed_prints +(** return the delayed print actions and reset them *) val set_delayed_prints : delayed_prints -> unit (** set the delayed print actions *)