Revision 850f427fc4f829604b95c8c3d15b29bfb180f89e authored by Pierre-Yves Strub on 21 February 2018, 16:09:18 UTC, committed by Pierre-Yves Strub on 21 February 2018, 16:09:18 UTC
1 parent 6c010d0
ecGState.ml
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-C-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
open EcMaps
(* -------------------------------------------------------------------- *)
type nid_t = EcUid.uid
type loglevel = [`Debug | `Info | `Warning | `Critical]
type notifier = {
nt_id : nid_t;
nt_cb : loglevel -> string Lazy.t -> unit;
}
type gstate = {
mutable gs_flags : bool Mstr.t;
mutable gs_notifiers : notifier list;
mutable gs_loglevel : loglevel;
}
(* -------------------------------------------------------------------- *)
let create () : gstate =
{ gs_flags = Mstr.empty;
gs_notifiers = [];
gs_loglevel = `Info; }
(* -------------------------------------------------------------------- *)
let copy (gs : gstate) : gstate =
{ gs_flags = gs.gs_flags ;
gs_notifiers = gs.gs_notifiers;
gs_loglevel = gs.gs_loglevel ; }
(* -------------------------------------------------------------------- *)
let from_flags (flags : (string * bool) list) : gstate =
let gstate = create () in
{ gstate with gs_flags = Mstr.of_list flags; }
(* -------------------------------------------------------------------- *)
let getflag ?(default = false) (name : string) (g : gstate) =
Mstr.find_def default name g.gs_flags
(* -------------------------------------------------------------------- *)
let setflag (name : string) (value : bool) (g : gstate) =
g.gs_flags <- Mstr.add name value g.gs_flags
(* -------------------------------------------------------------------- *)
let add_notifier (notifier : loglevel -> string Lazy.t -> unit) (gs : gstate) =
let notifier = { nt_id = EcUid.unique (); nt_cb = notifier; } in
gs.gs_notifiers <- notifier :: gs.gs_notifiers; notifier.nt_id
(* -------------------------------------------------------------------- *)
let rem_notifier (nid : nid_t) (gs : gstate) =
gs.gs_notifiers <- List.filter (fun nt -> nt.nt_id = nid) gs.gs_notifiers
(* -------------------------------------------------------------------- *)
let loglevel (gs : gstate) =
gs.gs_loglevel
(* -------------------------------------------------------------------- *)
let set_loglevel (lvl : loglevel) (gs : gstate) =
gs.gs_loglevel <- lvl
(* -------------------------------------------------------------------- *)
let int_of_loglevel = function
| `Debug -> 0
| `Info -> 1
| `Warning -> 2
| `Critical -> 3
let accept_log ~(level:loglevel) ~(wanted:loglevel) =
int_of_loglevel level <= int_of_loglevel wanted
(* -------------------------------------------------------------------- *)
let string_of_loglevel = function
| `Debug -> "debug"
| `Info -> "info"
| `Warning -> "warning"
| `Critical -> "critical"
(* -------------------------------------------------------------------- *)
let max_loglevel x1 x2 =
let i1 = int_of_loglevel x1 in
let i2 = int_of_loglevel x2 in
if i1 < i2 then x2 else x1
(* -------------------------------------------------------------------- *)
let notify (lvl : loglevel) (msg : string Lazy.t) (gs : gstate) =
let do1 (notifier : notifier) =
try notifier.nt_cb lvl msg
with _ -> ()
in
if accept_log ~level:gs.gs_loglevel ~wanted:lvl then
List.iter do1 gs.gs_notifiers
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...