Something went wrong. Try again.
forked from coq/coq
Something went wrong. Try again.
123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125(************************************************************************)(* * The Rocq Prover / The Rocq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)
open Xml_datatype
type level = | Debug | Info | Notice | Warning | Error
let pp_lvl fmt lvl = let open Format in match lvl with | Error -> fprintf fmt "Error: " | Info -> fprintf fmt "Info: " | Debug -> fprintf fmt "Debug: " | Warning -> fprintf fmt "Warning: " | Notice -> fprintf fmt ""
type doc_id = inttype route_id = int
type feedback_content = | Processed | Incomplete | Complete | ProcessingIn of string | InProgress of int | WorkerStatus of string * string | AddedAxiom | GlobRef of Loc.t * string * string * string * string | GlobDef of Loc.t * string * string * string | FileDependency of string option * string | FileLoaded of string * string (* Extra metadata *) | Custom of Loc.t option * string * xml (* Generic messages *) | Message of level * Loc.t option * Quickfix.t list * Pp.t
type feedback = { doc_id : doc_id; (* The document being concerned *) span_id : Stateid.t; route : route_id; contents : feedback_content;}
(** Feeders *)let feeders : (int, feedback -> unit) Hashtbl.t = Hashtbl.create 7
let add_feeder = let f_id = ref 0 in fun f -> incr f_id; Hashtbl.add feeders !f_id f; !f_id
let del_feeder fid = Hashtbl.remove feeders fid
let default_route = 0let span_id = ref Stateid.dummylet doc_id = ref 0let feedback_route = ref default_route
let set_id_for_feedback ?(route=default_route) d i = doc_id := d; span_id := i; feedback_route := route
let warn_no_listeners = ref truelet feedback ?did ?id ?route what = let m = { contents = what; route = Option.default !feedback_route route; doc_id = Option.default !doc_id did; span_id = Option.default !span_id id; } in if !warn_no_listeners && Hashtbl.length feeders = 0 then begin Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!"; match m.contents with | Message (lvl,_,_,msg) -> Format.eprintf "%a%a" pp_lvl lvl Pp.pp_with msg | _ -> () end ; Hashtbl.iter (fun _ f -> f m) feeders
(* Logging messages *)let feedback_logger ?loc ?(quickfix=[]) lvl msg = feedback ~route:!feedback_route ~id:!span_id (Message (lvl, loc, quickfix, msg))
let msg_info ?loc x = feedback_logger ?loc Info xlet msg_notice ?loc x = feedback_logger ?loc Notice xlet msg_warning ?loc ?quickfix x = feedback_logger ?loc ?quickfix Warning x(* let msg_error ?loc x = feedback_logger ?loc Error x *)let msg_debug ?loc x = feedback_logger ?loc Debug x
(* Helper for tools willing to understand only the messages *)let console_feedback_listener fmt = let open Format in let pp_loc fmt = function | None -> () | Some loc -> Pp.pp_with fmt Pp.(Loc.pr loc ++ str ":" ++ fnl()) in let checker_feed (fb : feedback) = match fb.contents with | Processed -> () | Incomplete -> () | Complete -> () | ProcessingIn _ -> () | InProgress _ -> () | WorkerStatus (_,_) -> () | AddedAxiom -> () | GlobRef (_,_,_,_,_) -> () | GlobDef (_,_,_,_) -> () | FileDependency (_,_) -> () | FileLoaded (_,_) -> () | Custom (_,_,_) -> () | Message (lvl,loc,_,msg) -> fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg in checker_feed