diff --git a/infer/src/backend/printer.ml b/infer/src/backend/printer.ml index 212e13e47..5000167ba 100644 --- a/infer/src/backend/printer.ml +++ b/infer/src/backend/printer.ml @@ -170,13 +170,11 @@ end (** Execute the delayed print actions *) let force_delayed_prints () = - Config.forcing_delayed_prints := true ; F.fprintf !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 () ; - Config.forcing_delayed_prints := false + L.reset_delayed_prints () (** Start a session, and create a new html fine for the node if it does not exist yet *) diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 7dccbc3df..cbd3ca6e3 100644 --- a/infer/src/base/Config.ml +++ b/infer/src/base/Config.ml @@ -3029,9 +3029,6 @@ let run_in_footprint_mode f x = set_reference_and_call_function footprint true f let run_in_re_execution_mode f x = set_reference_and_call_function footprint false f x -(** Set in the middle of forcing delayed prints *) -let forcing_delayed_prints = ref false - (** if true, user simple pretty printing *) let pp_simple = ref true diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 0507df99d..f978ef63e 100644 --- a/infer/src/base/Config.mli +++ b/infer/src/base/Config.mli @@ -680,8 +680,6 @@ val run_in_re_execution_mode : ('a -> 'b) -> 'a -> 'b (** Call f x with footprint set to false. Restore the initial value of footprint also in case of exception. *) -val forcing_delayed_prints : bool ref - val pp_simple : bool ref (** {2 Global variables with initial values specified by command-line options} *) diff --git a/infer/src/biabduction/Prop.ml b/infer/src/biabduction/Prop.ml index 194f1650e..92c811f2d 100644 --- a/infer/src/biabduction/Prop.ml +++ b/infer/src/biabduction/Prop.ml @@ -318,7 +318,7 @@ let prop_pred_env prop = (** Pretty print a proposition. *) let pp_prop pe0 f prop = let pe = prop_update_obj_sub pe0 prop in - let do_print f () = + let do_print f = let subl = Sil.sub_to_list prop.sub in (* since prop diff is based on physical equality, we need to extract the sub verbatim *) let pi = prop.pi in @@ -342,11 +342,12 @@ let pp_prop pe0 f prop = (pp_footprint_simple pe env) prop pp_predicates () else F.fprintf f "%a%a%a" pp_pure () (pp_sigma pe) prop.sigma (pp_footprint pe) prop in - if !Config.forcing_delayed_prints then - (* print in html mode *) - F.fprintf f "%a%a%a" Io_infer.Html.pp_start_color Pp.Blue do_print () - Io_infer.Html.pp_end_color () - else (* print in text mode *) do_print f () + match pe0.Pp.kind with + | Pp.HTML -> + F.fprintf f "%a%t%a" Io_infer.Html.pp_start_color Pp.Blue do_print Io_infer.Html.pp_end_color + () + | TEXT -> + do_print f let pp_prop_with_typ pe f p = pp_prop {pe with opt= SIM_WITH_TYP} f p