package why3find

  1. Overview
  2. Docs

Source file log.ml

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
(**************************************************************************)
(*                                                                        *)
(*  SPDX-License-Identifier LGPL-2.1                                      *)
(*  Copyright (C)                                                         *)
(*  CEA (Commissariat à l'énergie atomique et aux énergies alternatives)  *)
(*                                                                        *)
(**************************************************************************)

(* -------------------------------------------------------------------------- *)
(* --- Logging Facilities                                                 --- *)
(* -------------------------------------------------------------------------- *)

let is_log_on = ref false
let warnings = ref 0
let errors = ref 0
let summary = Queue.create ()

type level = [ `Message | `Warning | `Error ]

let pp_stdout = ref (fun pp -> pp Format.std_formatter)
let pp_stderr = ref (fun pp -> pp Format.err_formatter)

let summarize_err pp = Queue.push pp summary ; !pp_stderr pp

let output level pp =
  Utils.flush ();
  match level with
  | `Message ->
    Format.kdprintf !pp_stdout "@[<hov>%t@]@." pp
  | `Warning ->
    incr warnings ;
    Format.kdprintf summarize_err
      "@[<hov>@{<bold>@{<bright magenta>Warning:@}@} %t@]@." pp
  | `Error ->
    incr errors ;
    Format.kdprintf summarize_err
      "@[<hov>@{<bold>@{<bright red>Error:@}@} %t@]@." pp

let set_log b =
  is_log_on := b

let emit ?(level=`Message) msg =
  if !is_log_on
  then Format.kdprintf (output level) msg
  else Format.ifprintf Format.std_formatter msg

let printf msg = Format.kdprintf !pp_stdout msg
let eprintf msg = Format.kdprintf !pp_stderr msg
let message msg = emit ~level:`Message msg
let warning msg = emit ~level:`Warning msg
let error   msg = emit ~level:`Error   msg

let summary () =
  if !is_log_on then
    let wrn = !warnings in
    if wrn > 0 then
      begin
        Utils.flush ();
        if not Utils.tty || Utils.overflows () then
          begin
            eprintf "Summary:@.";
            Queue.iter !pp_stderr summary ;
          end ;
        printf "Emitted %d warning%a" wrn Utils.pp_s wrn ;
        let err = !errors in
        if err > 0 then
          printf ", %d error%a" err Utils.pp_s err ;
        printf "@."
      end

let exit_summary () =
  try summary () with _ -> ()

let () =
  at_exit exit_summary