Logging/Printer: better code

Reviewed By: jeremydubreil Differential Revision: D8397761 fbshipit-source-id: 7d7b309
7 years ago · 4eef0d90c8
parent 0563578b43
commit 4eef0d90c8
18 changed files with 128 additions and 338 deletions
--- a/infer/src/IR/PredSymb.ml
+++ b/infer/src/IR/PredSymb.ml
@ -257,5 +257,7 @@ let to_string pe = function
      "WONT_LEAK"


+let pp pe fmt a = F.pp_print_string fmt (to_string pe a)
+
 (** dump an attribute *)
-let d_attribute (a: t) = L.add_print_action (L.PTattribute, Obj.repr a)
+let d_attribute (a: t) = L.add_print_with_pe pp a
--- a/infer/src/IR/Procdesc.ml
+++ b/infer/src/IR/Procdesc.ml
@ -168,7 +168,7 @@ module Node = struct

  (** Print extended instructions for the node,
      highlighting the given subinstruction if present *)
-  let pp_instrs pe0 ~sub_instrs instro fmt node =
+  let pp_instrs pe0 ~sub_instrs ~instro fmt node =
    if sub_instrs then
      let pe =
        match instro with None -> pe0 | Some instr -> Pp.extend_colormap pe0 (Obj.repr instr) Red
@ -196,7 +196,7 @@ module Node = struct

  (** Dump extended instructions for the node *)
  let d_instrs ~(sub_instrs: bool) (curr_instr: Sil.instr option) (node: t) =
-    L.add_print_action (L.PTnode_instrs, Obj.repr (sub_instrs, curr_instr, node))
+    L.add_print_with_pe ~color:Pp.Green (pp_instrs ~sub_instrs ~instro:curr_instr) node


  (** Return a description of the cfg node *)
@ -216,7 +216,7 @@ module Node = struct
      | Join_node ->
          "Join"
    in
-    let pp fmt = F.fprintf fmt "%s@.%a" str (pp_instrs pe None ~sub_instrs:true) node in
+    let pp fmt = F.fprintf fmt "%s@.%a" str (pp_instrs pe ~instro:None ~sub_instrs:true) node in
    F.asprintf "%t" pp
 end

--- a/infer/src/IR/Procdesc.mli
+++ b/infer/src/IR/Procdesc.mli
@ -99,7 +99,8 @@ module Node : sig
  val pp_id : Format.formatter -> id -> unit
  (** Pretty print a node id *)

-  val pp_instrs : Pp.env -> sub_instrs:bool -> Sil.instr option -> Format.formatter -> t -> unit
+  val pp_instrs :
+    Pp.env -> sub_instrs:bool -> instro:Sil.instr option -> Format.formatter -> t -> unit
  (** Print extended instructions for the node,
      highlighting the given subinstruction if present *)
 end
--- a/infer/src/IR/Pvar.ml
+++ b/infer/src/IR/Pvar.ml
@ -97,7 +97,7 @@ let pp pe f pv =


 (** Dump a program variable. *)
-let d (pvar: t) = L.add_print_action (L.PTpvar, Obj.repr pvar)
+let d (pvar: t) = L.add_print_with_pe pp pvar

 let get_name pv = pv.pv_name

--- a/infer/src/IR/Sil.ml
+++ b/infer/src/IR/Sil.ml
@ -274,13 +274,13 @@ let pp_exp_printenv pe0 f e0 =


 (** dump an expression. *)
-let d_exp (e: Exp.t) = L.add_print_action (L.PTexp, Obj.repr e)
+let d_exp (e: Exp.t) = L.add_print_with_pe pp_exp_printenv e

 (** Pretty print a list of expressions. *)
 let pp_exp_list pe f expl = Pp.seq (pp_exp_printenv pe) f expl

 (** dump a list of expressions. *)
-let d_exp_list (el: Exp.t list) = L.add_print_action (L.PTexp_list, Obj.repr el)
+let d_exp_list (el: Exp.t list) = L.add_print_with_pe pp_exp_list el

 let pp_texp pe f = function
  | Exp.Sizeof {typ; nbytes; dynamic_length; subtype} ->
@ -304,7 +304,7 @@ let pp_texp_full pe f = function


 (** Dump a type expression with all the details. *)
-let d_texp_full (te: Exp.t) = L.add_print_action (L.PTtexp_full, Obj.repr te)
+let d_texp_full (te: Exp.t) = L.add_print_with_pe pp_texp_full te

 (** Pretty print an offset *)
 let pp_offset pe f = function
@ -328,7 +328,7 @@ let rec pp_offset_list pe f = function


 (** Dump a list of offsets *)
-let d_offset_list (offl: offset list) = L.add_print_action (L.PToff_list, Obj.repr offl)
+let d_offset_list (offl: offset list) = L.add_print_with_pe pp_offset_list offl

 let pp_exp_typ pe f (e, t) = F.fprintf f "%a:%a" (pp_exp_printenv pe) e (Typ.pp pe) t

@ -430,7 +430,7 @@ let add_with_block_parameters_flag instr =
 let is_block_pvar pvar = Typ.has_block_prefix (Mangled.to_string (Pvar.get_name pvar))

 (** Dump an instruction. *)
-let d_instr (i: instr) = L.add_print_action (L.PTinstr, Obj.repr i)
+let d_instr (i: instr) = L.add_print_with_pe ~color:Pp.Green pp_instr i

 let pp_atom pe0 f a =
  let pe, changed = color_pre_wrapper pe0 f a in
@ -449,7 +449,7 @@ let pp_atom pe0 f a =


 (** dump an atom *)
-let d_atom (a: atom) = L.add_print_action (L.PTatom, Obj.repr a)
+let d_atom (a: atom) = L.add_print_with_pe pp_atom a

 let pp_lseg_kind f = function Lseg_NE -> F.pp_print_string f "ne" | Lseg_PE -> ()

@ -881,13 +881,10 @@ let pp_hpara_dll pe f = pp_hpara_dll_env pe None f
 let pp_hpred pe f = pp_hpred_env pe None f

 (** dump a strexp. *)
-let d_sexp (se: strexp) = L.add_print_action (L.PTsexp, Obj.repr se)
-
-(** Pretty print a list of expressions. *)
-let pp_sexp_list pe f sel = (Pp.seq (fun f se -> (pp_sexp pe) f se)) f sel
+let d_sexp (se: strexp) = L.add_print_with_pe pp_sexp se

 (** dump a hpred. *)
-let d_hpred (hpred: hpred) = L.add_print_action (L.PThpred, Obj.repr hpred)
+let d_hpred (hpred: hpred) = L.add_print_with_pe pp_hpred hpred

 (** {2 Functions for traversing SIL data types} *)

--- a/infer/src/IR/Sil.mli
+++ b/infer/src/IR/Sil.mli
@ -270,21 +270,12 @@ val pp_texp_full : Pp.env -> F.formatter -> Exp.t -> unit
 val d_texp_full : Exp.t -> unit
 (** Dump a type expression with all the details. *)

-val pp_exp_list : Pp.env -> F.formatter -> Exp.t list -> unit
-(** Pretty print a list of expressions. *)
-
 val d_exp_list : Exp.t list -> unit
 (** Dump a list of expressions. *)

-val pp_offset : Pp.env -> F.formatter -> offset -> unit
-(** Pretty print an offset *)
-
 val offset_to_string : offset -> string
 (** Convert an offset to a string *)

-val pp_offset_list : Pp.env -> F.formatter -> offset list -> unit
-(** Pretty print a list of offsets *)
-
 val d_offset_list : offset list -> unit
 (** Dump a list of offsets *)

@ -318,9 +309,6 @@ val pp_sexp : Pp.env -> F.formatter -> strexp -> unit
 val d_sexp : strexp -> unit
 (** Dump a strexp. *)

-val pp_sexp_list : Pp.env -> F.formatter -> strexp list -> unit
-(** Pretty print a strexp list. *)
-
 val pp_hpred : Pp.env -> F.formatter -> hpred -> unit
 (** Pretty print a hpred. *)

--- a/infer/src/IR/Typ.ml
+++ b/infer/src/IR/Typ.ml
@ -490,10 +490,13 @@ module Name = struct
 end

 (** dump a type with all the details. *)
-let d_full (t: t) = L.add_print_action (L.PTtyp_full, Obj.repr t)
+let d_full (t: t) = L.add_print_with_pe pp_full t

 (** dump a list of types. *)
-let d_list (tl: t list) = L.add_print_action (L.PTtyp_list, Obj.repr tl)
+let d_list (tl: t list) =
+  let pp pe = Pp.seq (pp pe) in
+  L.add_print_with_pe pp tl
+

 let name typ = match typ.desc with Tstruct name -> Some name | _ -> None

--- a/infer/src/backend/ondemand.ml
+++ b/infer/src/backend/ondemand.ml
@ -75,7 +75,7 @@ let procedure_should_be_analyzed proc_name =
 type global_state =
  { abs_val: int
  ; abstraction_rules: Abs.rules
-  ; delayed_prints: L.print_action list
+  ; delayed_prints: L.delayed_prints
  ; footprint_mode: bool
  ; html_formatter: F.formatter
  ; name_generator: Ident.NameGenerator.t
--- a/infer/src/backend/printer.ml
+++ b/infer/src/backend/printer.ml
@ -163,164 +163,12 @@ end
 (* =============== END of module NodesHtml =============== *)
 (* =============== Printing functions =============== *)

-(** Execute the delayed print actions *)
-let force_delayed_print fmt =
-  let pe_default = if Config.write_html then Pp.html Black else Pp.text in
-  function
-    | L.PTatom, a ->
-        let a : Sil.atom = Obj.obj a in
-        Sil.pp_atom pe_default fmt a
-    | L.PTattribute, a ->
-        let a : PredSymb.t = Obj.obj a in
-        F.pp_print_string fmt (PredSymb.to_string pe_default a)
-    | L.PTdecrease_indent, n ->
-        let n : int = Obj.obj n in
-        for _ = 1 to n do F.fprintf fmt "@]" done
-    | L.PTexp, e ->
-        let e : Exp.t = Obj.obj e in
-        Sil.pp_exp_printenv pe_default fmt e
-    | L.PTexp_list, el ->
-        let el : Exp.t list = Obj.obj el in
-        Sil.pp_exp_list pe_default fmt el
-    | L.PThpred, hpred ->
-        let hpred : Sil.hpred = Obj.obj hpred in
-        Sil.pp_hpred pe_default fmt hpred
-    | L.PTincrease_indent, n ->
-        let n : int = Obj.obj n in
-        F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
-    | L.PTinstr, i ->
-        let i : Sil.instr = Obj.obj i in
-        if Config.write_html then
-          F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
-            (Sil.pp_instr (Pp.html Green))
-            i Io_infer.Html.pp_end_color ()
-        else Sil.pp_instr Pp.text fmt i
-    | L.PTinstr_list, il ->
-        let il : Instrs.not_reversed_t = Obj.obj il in
-        if Config.write_html then
-          F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
-            (Instrs.pp (Pp.html Green))
-            il Io_infer.Html.pp_end_color ()
-        else Instrs.pp Pp.text fmt il
-    | L.PTjprop_list, shallow_jpl ->
-        let (shallow: bool), (jpl: Prop.normal BiabductionSummary.Jprop.t list) =
-          Obj.obj shallow_jpl
-        in
-        BiabductionSummary.Jprop.pp_list pe_default ~shallow fmt jpl
-    | L.PTjprop_short, jp ->
-        let jp : Prop.normal BiabductionSummary.Jprop.t = Obj.obj jp in
-        BiabductionSummary.Jprop.pp_short pe_default fmt jp
-    | L.PTloc, loc ->
-        let loc : Location.t = Obj.obj loc in
-        Location.pp fmt loc
-    | L.PTnode_instrs, b_n ->
-        let (b: bool), (io: Sil.instr option), (n: Procdesc.Node.t) = Obj.obj b_n in
-        if Config.write_html then
-          F.fprintf fmt "%a%a%a" Io_infer.Html.pp_start_color Pp.Green
-            (Procdesc.Node.pp_instrs (Pp.html Green) io ~sub_instrs:b)
-            n Io_infer.Html.pp_end_color ()
-        else Procdesc.Node.pp_instrs Pp.text io ~sub_instrs:b fmt n
-    | L.PToff, off ->
-        let off : Sil.offset = Obj.obj off in
-        Sil.pp_offset pe_default fmt off
-    | L.PToff_list, offl ->
-        let offl : Sil.offset list = Obj.obj offl in
-        Sil.pp_offset_list pe_default fmt offl
-    | L.PTpathset, ps ->
-        let ps : Paths.PathSet.t = Obj.obj ps in
-        F.fprintf fmt "%a@\n" (Paths.PathSet.pp pe_default) ps
-    | L.PTpi, pi ->
-        let pi : Sil.atom list = Obj.obj pi in
-        Prop.pp_pi pe_default fmt pi
-    | L.PTpath, path ->
-        let path : Paths.Path.t = Obj.obj path in
-        Paths.Path.pp fmt path
-    | L.PTprop, p ->
-        let p : Prop.normal Prop.t = Obj.obj p in
-        Prop.pp_prop pe_default fmt p
-    | L.PTproplist, x ->
-        let (p: Prop.normal Prop.t), (pl: Prop.normal Prop.t list) = Obj.obj x in
-        Propgraph.pp_proplist pe_default "PROP" (p, false) fmt pl
-    | L.PTprop_list_with_typ, plist ->
-        let pl : Prop.normal Prop.t list = Obj.obj plist in
-        Prop.pp_proplist_with_typ pe_default fmt pl
-    | L.PTprop_with_typ, p ->
-        let p : Prop.normal Prop.t = Obj.obj p in
-        Prop.pp_prop_with_typ pe_default fmt p
-    | L.PTpvar, pvar ->
-        let pvar : Pvar.t = Obj.obj pvar in
-        Pvar.pp pe_default fmt pvar
-    | L.PTsexp, se ->
-        let se : Sil.strexp = Obj.obj se in
-        Sil.pp_sexp pe_default fmt se
-    | L.PTsexp_list, sel ->
-        let sel : Sil.strexp list = Obj.obj sel in
-        Sil.pp_sexp_list pe_default fmt sel
-    | L.PTsigma, sigma ->
-        let sigma : Sil.hpred list = Obj.obj sigma in
-        Prop.pp_sigma pe_default fmt sigma
-    | L.PTspec, spec ->
-        let spec : Prop.normal BiabductionSummary.spec = Obj.obj spec in
-        BiabductionSummary.pp_spec
-          (if Config.write_html then Pp.html Blue else Pp.text)
-          None fmt spec
-    | L.PTstr, s ->
-        let s : string = Obj.obj s in
-        F.pp_print_string fmt s
-    | L.PTstr_color, s ->
-        let (s: string), (c: Pp.color) = Obj.obj s in
-        if Config.write_html then
-          F.fprintf fmt "%a%s%a" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color ()
-        else F.pp_print_string fmt s
-    | L.PTstrln, s ->
-        let s : string = Obj.obj s in
-        F.fprintf fmt "%s@\n" s
-    | L.PTstrln_color, s ->
-        let (s: string), (c: Pp.color) = Obj.obj s in
-        if Config.write_html then
-          F.fprintf fmt "%a%s%a@\n" Io_infer.Html.pp_start_color c s Io_infer.Html.pp_end_color ()
-        else F.fprintf fmt "%s@\n" s
-    | L.PTsub, sub ->
-        let sub : Sil.subst = Obj.obj sub in
-        Prop.pp_sub pe_default fmt sub
-    | L.PTtexp_full, te ->
-        let te : Exp.t = Obj.obj te in
-        Sil.pp_texp_full pe_default fmt te
-    | L.PTtyp_full, t ->
-        let t : Typ.t = Obj.obj t in
-        Typ.pp_full pe_default fmt t
-    | L.PTtyp_list, tl ->
-        let tl : Typ.t list = Obj.obj tl in
-        Pp.seq (Typ.pp pe_default) fmt tl
-    | L.PTerror, s ->
-        let s : string = Obj.obj s in
-        if Config.write_html then
-          F.fprintf fmt "%aERROR: %s%a" Io_infer.Html.pp_start_color Pp.Red s
-            Io_infer.Html.pp_end_color ()
-        else F.fprintf fmt "ERROR: %s" s
-    | L.PTwarning, s ->
-        let s : string = Obj.obj s in
-        if Config.write_html then
-          F.fprintf fmt "%aWARNING: %s%a" Io_infer.Html.pp_start_color Pp.Orange s
-            Io_infer.Html.pp_end_color ()
-        else F.fprintf fmt "WARNING: %s" s
-    | L.PTinfo, s ->
-        let s : string = Obj.obj s in
-        if Config.write_html then
-          F.fprintf fmt "%aINFO: %s%a" Io_infer.Html.pp_start_color Pp.Blue s
-            Io_infer.Html.pp_end_color ()
-        else F.fprintf fmt "INFO: %s" s
-
-
-(** Set printer hook as soon as this module is loaded *)
-let () = L.printer_hook := force_delayed_print
-
 (** Execute the delayed print actions *)
 let force_delayed_prints () =
  Config.forcing_delayed_prints := true ;
  F.fprintf !curr_html_formatter "@?" ;
  (* flush html stream *)
-  List.iter ~f:(force_delayed_print !curr_html_formatter) (List.rev (L.get_delayed_prints ())) ;
+  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
@ -337,7 +185,7 @@ let start_session ~pp_name node (loc: Location.t) proc_name session source =
  then
    F.fprintf !curr_html_formatter "%a<LISTING>%a</LISTING>%a" Io_infer.Html.pp_start_color
      Pp.Green
-      (Procdesc.Node.pp_instrs (Pp.html Green) None ~sub_instrs:true)
+      (Procdesc.Node.pp_instrs (Pp.html Green) ~instro:None ~sub_instrs:true)
      node Io_infer.Html.pp_end_color () ;
  F.fprintf !curr_html_formatter "%a%a %t" Io_infer.Html.pp_hline ()
    (Io_infer.Html.pp_session_link source ~with_name:true [".."] ~proc_name)
--- a/infer/src/base/Logging.ml
+++ b/infer/src/base/Logging.ml
@ -348,61 +348,78 @@ let setup_log_file () =
           ============================================================"


-(** type of printable elements *)
-type print_type =
-  | PTatom
-  | PTattribute
-  | PTdecrease_indent
-  | PTexp
-  | PTexp_list
-  | PThpred
-  | PTincrease_indent
-  | PTinstr
-  | PTinstr_list
-  | PTjprop_list
-  | PTjprop_short
-  | PTloc
-  | PTnode_instrs
-  | PToff
-  | PToff_list
-  | PTpath
-  | PTprop
-  | PTproplist
-  | PTprop_list_with_typ
-  | PTprop_with_typ
-  | PTpvar
-  | PTspec
-  | PTstr
-  | PTstr_color
-  | PTstrln
-  | PTstrln_color
-  | PTpathset
-  | PTpi
-  | PTsexp
-  | PTsexp_list
-  | PTsigma
-  | PTtexp_full
-  | PTsub
-  | PTtyp_full
-  | PTtyp_list
-  | PTwarning
-  | PTerror
-  | PTinfo
-
 (** delayable print action *)
-type print_action = print_type * Obj.t  (** data to be printed *)
+type print_action =
+  | PTdecrease_indent: int -> print_action
+  | PTincrease_indent: int -> print_action
+  | PTstr: string -> print_action
+  | PTstr_color: string * Pp.color -> print_action
+  | PTstrln: string -> print_action
+  | PTstrln_color: string * Pp.color -> print_action
+  | PTwarning: string -> print_action
+  | PTerror: string -> print_action
+  | PTinfo: string -> print_action
+  | PT_generic: (Format.formatter -> 'a -> unit) * 'a -> print_action
+  | PT_generic_with_pe:
+      Pp.color option * (Pp.env -> Format.formatter -> 'a -> unit) * 'a
+      -> print_action
+
+type delayed_prints = print_action list

 let delayed_actions = ref []

-(** hook for the current printer of delayed print actions *)
-let printer_hook = ref (fun _ -> Die.(die InternalError) "uninitialized printer hook")
+let pp_with_html_color color pp fmt x =
+  F.fprintf fmt "<span class='%s'>%a</span>" (Pp.color_string color) pp x
+
+
+let pp_maybe_with_color color pp fmt x =
+  if Config.write_html then pp fmt x else pp_with_html_color color pp fmt x
+
+
+(** Execute the delayed print actions *)
+let force_delayed_print fmt = function
+  | PTdecrease_indent n ->
+      for _ = 1 to n do F.fprintf fmt "@]" done
+  | PTincrease_indent n ->
+      F.fprintf fmt "%s@[" (String.make (2 * n) ' ')
+  | PTstr s ->
+      F.pp_print_string fmt s
+  | PTstr_color (s, c) ->
+      pp_maybe_with_color c F.pp_print_string fmt s
+  | PTstrln s ->
+      F.fprintf fmt "%s@\n" s
+  | PTstrln_color (s, c) ->
+      F.fprintf fmt "%a@\n" (pp_maybe_with_color c F.pp_print_string) s
+  | PTerror s ->
+      pp_maybe_with_color Pp.Red (fun fmt -> F.fprintf fmt "ERROR: %s") fmt s
+  | PTwarning s ->
+      pp_maybe_with_color Pp.Orange (fun fmt -> F.fprintf fmt "WARNING: %s") fmt s
+  | PTinfo s ->
+      pp_maybe_with_color Pp.Blue (fun fmt -> F.fprintf fmt "INFO: %s") fmt s
+  | PT_generic (pp, x) ->
+      pp fmt x
+  | PT_generic_with_pe (None, pp, x) ->
+      let pe_default = if Config.write_html then Pp.html Black else Pp.text in
+      pp pe_default fmt x
+  | PT_generic_with_pe (Some color, pp, x) ->
+      if Config.write_html then pp_with_html_color color (pp (Pp.html color)) fmt x
+      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)
+

 (** extend the current print log *)
 let add_print_action pact =
  if Config.write_html then delayed_actions := pact :: !delayed_actions
  else if not Config.only_cheap_debug then
-    Option.iter !log_file ~f:(function file_fmt, _ -> !printer_hook file_fmt pact)
+    Option.iter !log_file ~f:(function file_fmt, _ -> force_delayed_print file_fmt pact)
+
+
+let add_print pp x = add_print_action (PT_generic (pp, x))

+let add_print_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 := []
@ -414,38 +431,38 @@ let get_delayed_prints () = !delayed_actions
 let set_delayed_prints new_delayed_actions = delayed_actions := new_delayed_actions

 (** dump a string *)
-let d_str (s: string) = add_print_action (PTstr, Obj.repr s)
+let d_str (s: string) = add_print_action (PTstr s)

 (** dump a string with the given color *)
-let d_str_color (c: Pp.color) (s: string) = add_print_action (PTstr_color, Obj.repr (s, c))
+let d_str_color (c: Pp.color) (s: string) = add_print_action (PTstr_color (s, c))

 (** dump an error string *)
-let d_error (s: string) = add_print_action (PTerror, Obj.repr s)
+let d_error (s: string) = add_print_action (PTerror s)

 (** dump a warning string *)
-let d_warning (s: string) = add_print_action (PTwarning, Obj.repr s)
+let d_warning (s: string) = add_print_action (PTwarning s)

 (** dump an info string *)
-let d_info (s: string) = add_print_action (PTinfo, Obj.repr s)
+let d_info (s: string) = add_print_action (PTinfo s)

 (** dump a string plus newline *)
-let d_strln (s: string) = add_print_action (PTstrln, Obj.repr s)
+let d_strln (s: string) = add_print_action (PTstrln s)

 (** dump a string plus newline with the given color *)
-let d_strln_color (c: Pp.color) (s: string) = add_print_action (PTstrln_color, Obj.repr (s, c))
+let d_strln_color (c: Pp.color) (s: string) = add_print_action (PTstrln_color (s, c))

 (** dump a newline *)
-let d_ln () = add_print_action (PTstrln, Obj.repr "")
+let d_ln () = add_print_action (PTstrln "")

 (** dump an indentation *)
 let d_indent indent =
-  let s = ref "" in
-  for _ = 1 to indent do s := "  " ^ !s done ;
-  if indent <> 0 then add_print_action (PTstr, Obj.repr !s)
+  if indent <> 0 then
+    let s = String.make (2 * indent) ' ' in
+    add_print_action (PTstr s)


 (** dump command to increase the indentation level *)
-let d_increase_indent (indent: int) = add_print_action (PTincrease_indent, Obj.repr indent)
+let d_increase_indent (indent: int) = add_print_action (PTincrease_indent indent)

 (** dump command to decrease the indentation level *)
-let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent, Obj.repr indent)
+let d_decrease_indent (indent: int) = add_print_action (PTdecrease_indent indent)
--- a/infer/src/base/Logging.mli
+++ b/infer/src/base/Logging.mli
@ -87,60 +87,18 @@ val reset_formatters : unit -> unit

 (** Delayed printing (HTML debug, ...) *)

-(** type of printable elements *)
-type print_type =
-  | PTatom
-  | PTattribute
-  | PTdecrease_indent
-  | PTexp
-  | PTexp_list
-  | PThpred
-  | PTincrease_indent
-  | PTinstr
-  | PTinstr_list
-  | PTjprop_list
-  | PTjprop_short
-  | PTloc
-  | PTnode_instrs
-  | PToff
-  | PToff_list
-  | PTpath
-  | PTprop
-  | PTproplist
-  | PTprop_list_with_typ
-  | PTprop_with_typ
-  | PTpvar
-  | PTspec
-  | PTstr
-  | PTstr_color
-  | PTstrln
-  | PTstrln_color
-  | PTpathset
-  | PTpi
-  | PTsexp
-  | PTsexp_list
-  | PTsigma
-  | PTtexp_full
-  | PTsub
-  | PTtyp_full
-  | PTtyp_list
-  | PTwarning
-  | PTerror
-  | PTinfo
-
-(** delayable print action *)
-type print_action = print_type * Obj.t  (** data to be printed *)
-
-val printer_hook : (F.formatter -> print_action -> unit) ref
-(** hook for the current printer of delayed print actions *)
-
-val add_print_action : print_action -> unit
-(** extend he current print log *)
-
-val get_delayed_prints : unit -> print_action list
+type delayed_prints
+
+val add_print : (F.formatter -> 'a -> unit) -> 'a -> unit
+
+val add_print_with_pe : ?color:Pp.color -> (Pp.env -> F.formatter -> 'a -> unit) -> 'a -> unit
+
+val force_delayed_prints : F.formatter -> delayed_prints -> unit
+
+val get_delayed_prints : unit -> delayed_prints
 (** return the delayed print actions *)

-val set_delayed_prints : print_action list -> unit
+val set_delayed_prints : delayed_prints -> unit
 (** set the delayed print actions *)

 val reset_delayed_prints : unit -> unit
--- a/infer/src/biabduction/BiabductionSummary.ml
+++ b/infer/src/biabduction/BiabductionSummary.ml
@ -60,7 +60,7 @@ module Jprop = struct
  let pp_short pe f jp = Prop.pp_prop pe f (to_prop jp)

  (** Dump the toplevel prop *)
-  let d_shallow (jp: Prop.normal t) = L.add_print_action (L.PTjprop_short, Obj.repr jp)
+  let d_shallow (jp: Prop.normal t) = L.add_print_with_pe pp_short jp

  (** Get identifies of the jprop *)
  let get_id = function Prop (n, _) -> n | Joined (n, _, _, _) -> n
@ -85,7 +85,7 @@ module Jprop = struct

  (** dump a joined prop list, the boolean indicates whether to print toplevel props only *)
  let d_list ~(shallow: bool) (jplist: Prop.normal t list) =
-    L.add_print_action (L.PTjprop_list, Obj.repr (shallow, jplist))
+    L.add_print_with_pe (pp_list ~shallow) jplist


  let rec gen_free_vars =
@ -264,7 +264,9 @@ let pp_spec pe num_opt fmt spec =


 (** Dump a spec *)
-let d_spec (spec: 'a spec) = L.add_print_action (L.PTspec, Obj.repr spec)
+let d_spec (spec: 'a spec) =
+  L.add_print (pp_spec (if Config.write_html then Pp.html Blue else Pp.text) None) spec
+

 let pp_specs pe fmt specs =
  let total = List.length specs in
--- a/infer/src/biabduction/BiabductionSummary.mli
+++ b/infer/src/biabduction/BiabductionSummary.mli
@ -37,12 +37,6 @@ module Jprop : sig
  val map : ('a Prop.t -> 'b Prop.t) -> 'a t -> 'b t
  (** map the function to each prop in the jprop, pointwise *)

-  val pp_list : Pp.env -> shallow:bool -> Format.formatter -> Prop.normal t list -> unit
-  (** Print a list of joined props, the boolean indicates whether to print subcomponents of joined props *)
-
-  val pp_short : Pp.env -> Format.formatter -> Prop.normal t -> unit
-  (** Print the toplevel prop *)
-
  val to_prop : 'a t -> 'a Prop.t
  (** Extract the toplevel jprop of a prop *)
 end
@ -70,15 +64,12 @@ end
 val normalized_specs_to_specs : NormSpec.t list -> Prop.normal spec list
 (** Cast a list of normalized specs to a list of specs *)

-val d_spec : 'a spec -> unit
+val d_spec : _ spec -> unit
 (** Dump a spec *)

 val spec_normalize : Tenv.t -> Prop.normal spec -> NormSpec.t
 (** Convert spec into normal form w.r.t. variable renaming *)

-val pp_spec : Pp.env -> (int * int) option -> Format.formatter -> Prop.normal spec -> unit
-(** Print the spec *)
-
 type phase = FOOTPRINT | RE_EXECUTION

 val equal_phase : phase -> phase -> bool
--- a/infer/src/biabduction/Paths.ml
+++ b/infer/src/biabduction/Paths.ml
@ -453,7 +453,7 @@ end = struct
    add_delayed path ; doit 0 fmt path ; print_delayed ()


-  let d p = L.add_print_action (L.PTpath, Obj.repr p)
+  let d p = L.add_print pp p

  let create_loc_trace path pos_opt : Errlog.loc_trace =
    let trace = ref [] in
@ -593,9 +593,6 @@ module PathSet : sig
  val partition : (Prop.normal Prop.t -> bool) -> t -> t * t
  (** partition a pathset on the prop component *)

-  val pp : Pp.env -> Format.formatter -> t -> unit
-  (** pretty print the pathset *)
-
  val size : t -> int
  (** number of elements in the pathset *)

@ -705,7 +702,10 @@ end = struct
    iter f ps


-  let d (ps: t) = L.add_print_action (L.PTpathset, Obj.repr ps)
+  let d (ps: t) =
+    let pp pe fmt ps = F.fprintf fmt "%a@\n" (pp pe) ps in
+    L.add_print_with_pe pp ps
+

  (** It's the caller's resposibility to ensure that Prop.prop_rename_primed_footprint_vars was called on the list *)
  let from_renamed_list (pl: ('a Prop.t * Path.t) list) : t =
--- a/infer/src/biabduction/Paths.mli
+++ b/infer/src/biabduction/Paths.mli
@ -56,9 +56,6 @@ module Path : sig
  val join : t -> t -> t
  (** join two paths *)

-  val pp : Format.formatter -> t -> unit
-  (** pretty print a path *)
-
  val pp_stats : Format.formatter -> t -> unit
    [@@warning "-32"]
  (** pretty print statistics of the path *)
@ -110,9 +107,6 @@ module PathSet : sig
  val partition : (Prop.normal Prop.t -> bool) -> t -> t * t
  (** partition a pathset on the prop component *)

-  val pp : Pp.env -> Format.formatter -> t -> unit
-  (** pretty print the pathset *)
-
  val size : t -> int
  (** number of elements in the pathset *)

--- a/infer/src/biabduction/Prop.ml
+++ b/infer/src/biabduction/Prop.ml
@ -153,7 +153,7 @@ let pp_sub pe f = function


 (** Dump a substitution. *)
-let d_sub (sub: Sil.subst) = L.add_print_action (PTsub, Obj.repr sub)
+let d_sub (sub: Sil.subst) = L.add_print_with_pe pp_sub sub

 let pp_sub_entry pe0 f entry =
  let pe, changed = Sil.color_pre_wrapper pe0 f entry in
@ -175,7 +175,7 @@ let pp_pi pe =


 (** Dump a pi. *)
-let d_pi (pi: pi) = L.add_print_action (PTpi, Obj.repr pi)
+let d_pi (pi: pi) = L.add_print_with_pe pp_pi pi

 (** Pretty print a sigma. *)
 let pp_sigma pe = Pp.semicolon_seq ~print_env:pe (Sil.pp_hpred pe)
@ -208,7 +208,7 @@ let pp_sigma_simple pe env fmt sigma =


 (** Dump a sigma. *)
-let d_sigma (sigma: sigma) = L.add_print_action (PTsigma, Obj.repr sigma)
+let d_sigma (sigma: sigma) = L.add_print_with_pe pp_sigma sigma

 (** Dump a pi and a sigma *)
 let d_pi_sigma pi sigma =
@ -345,7 +345,7 @@ let pp_prop pe0 f prop =
 let pp_prop_with_typ pe f p = pp_prop {pe with opt= SIM_WITH_TYP} f p

 (** Dump a proposition. *)
-let d_prop (prop: 'a t) = L.add_print_action (PTprop, Obj.repr prop)
+let d_prop (prop: 'a t) = L.add_print_with_pe pp_prop prop

 (** Print a list of propositions, prepending each one with the given string *)
 let pp_proplist_with_typ pe f plist =
@ -361,7 +361,7 @@ let pp_proplist_with_typ pe f plist =


 (** dump a proplist *)
-let d_proplist_with_typ (pl: 'a t list) = L.add_print_action (PTprop_list_with_typ, Obj.repr pl)
+let d_proplist_with_typ (pl: 'a t list) = L.add_print_with_pe pp_proplist_with_typ pl

 (** {1 Functions for computing free non-program variables} *)

--- a/infer/src/biabduction/Prop.mli
+++ b/infer/src/biabduction/Prop.mli
@ -49,9 +49,6 @@ val compare_prop : 'a t -> 'a t -> int
 val equal_sigma : sigma -> sigma -> bool
 (** Check the equality of two sigma's *)

-val pp_sub : Pp.env -> Format.formatter -> subst -> unit
-(** Pretty print a substitution. *)
-
 val d_sub : subst -> unit
 (** Dump a substitution. *)

@ -61,9 +58,6 @@ val pp_pi : Pp.env -> Format.formatter -> pi -> unit
 val d_pi : pi -> unit
 (** Dump a pi. *)

-val pp_sigma : Pp.env -> Format.formatter -> sigma -> unit
-(** Pretty print a sigma. *)
-
 val d_sigma : sigma -> unit
 (** Dump a sigma. *)

@ -80,18 +74,12 @@ val prop_update_obj_sub : Pp.env -> 'a t -> Pp.env
 val pp_prop : Pp.env -> Format.formatter -> 'a t -> unit
 (** Pretty print a proposition. *)

-val pp_prop_with_typ : Pp.env -> Format.formatter -> normal t -> unit
-(** Pretty print a proposition with type information *)
-
 val prop_pred_env : 'a t -> Sil.Predicates.env
 (** Create a predicate environment for a prop *)

 val d_prop : 'a t -> unit
 (** Dump a proposition. *)

-val pp_proplist_with_typ : Pp.env -> Format.formatter -> normal t list -> unit
-(** Pretty print a list propositions with type information *)
-
 val d_proplist_with_typ : 'a t list -> unit

 val pi_free_vars : pi -> Ident.t Sequence.t
--- a/infer/src/biabduction/Propgraph.ml
+++ b/infer/src/biabduction/Propgraph.ml
@ -262,4 +262,5 @@ let pp_proplist pe0 s (base_prop, extract_stack) f plist =

 (** dump a propset *)
 let d_proplist (p: 'a Prop.t) (pl: 'b Prop.t list) =
-  L.add_print_action (L.PTproplist, Obj.repr (p, pl))
+  let pp pe = pp_proplist pe "PROP" (p, false) in
+  L.add_print_with_pe pp pl