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
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
module Level = struct
type t =
| Error
| Warning
| Info
| Log
| Debug
end
module CallBack = struct
type t =
{ trace : string -> ?verbose:string -> string -> unit
; message : lvl:Level.t -> message:string -> unit
; diagnostics :
uri:Lang.LUri.File.t
-> version:int
-> Coq.Pp_t.t Lang.Diagnostic.t list
-> unit
; fileProgress :
uri:Lang.LUri.File.t -> version:int -> Progress.Info.t list -> unit
; perfData : uri:Lang.LUri.File.t -> version:int -> Perf.t -> unit
; serverVersion : ServerInfo.Version.t -> unit
; serverStatus : ServerInfo.Status.t -> unit
; execInfo :
uri:Lang.LUri.File.t -> version:int -> range:Lang.Range.t -> unit
}
let default =
{ trace = (fun _ ?verbose:_ _ -> ())
; message = (fun ~lvl:_ ~message:_ -> ())
; diagnostics = (fun ~uri:_ ~version:_ _ -> ())
; fileProgress = (fun ~uri:_ ~version:_ _ -> ())
; perfData = (fun ~uri:_ ~version:_ _ -> ())
; serverVersion = (fun _ -> ())
; serverStatus = (fun _ -> ())
; execInfo = (fun ~uri:_ ~version:_ ~range:_ -> ())
}
let cb = ref default
let set t = cb := t
end
(** Trace *)
module TraceValue = struct
type t =
| Off
| Messages
| Verbose
let of_string = function
| "messages" -> Ok Messages
| "verbose" -> Ok Verbose
| "off" -> Ok Off
| v -> Error ("TraceValue.parse: " ^ v)
let to_string = function
| Off -> "off"
| Messages -> "messages"
| Verbose -> "verbose"
end
module Log = struct
let trace_value = ref TraceValue.Off
let set_trace_value value = trace_value := value
let trace_ d ?verbose m =
match !trace_value with
| Off -> ()
| Messages -> !CallBack.cb.trace d ?verbose:None m
| Verbose -> !CallBack.cb.trace d ?verbose m
let trace d ?verbose = Format.kasprintf (fun m -> trace_ d ?verbose m)
let trace_object hdr obj =
trace hdr "[%s]: @[%a@]" hdr Yojson.Safe.(pretty_print ~std:false) obj
let pp_fb fmt (fb : Coq.Loc_t.t Coq.Message.t) =
let _lvl, { Coq.Message.Payload.msg; _ } = fb in
Format.fprintf fmt "%a" Coq.Pp_t.pp_with msg
let feedback part feedback =
if not (Lang.Compat.List.is_empty feedback) then
let pp_sep = Format.pp_print_cut in
let feedbacks =
Format.(asprintf "@[%a@]" (pp_print_list ~pp_sep pp_fb) feedback)
in
let verbose = Some feedbacks in
trace "feedback" ?verbose "received in %s" part
end
module Report = struct
let message_ ~io ~lvl ~message = io.CallBack.message ~lvl ~message
let msg ~io ~lvl = Format.kasprintf (fun m -> message_ ~io ~lvl ~message:m)
let diagnostics ~io ~uri ~version d = io.CallBack.diagnostics ~uri ~version d
let fileProgress ~io ~uri ~version d =
io.CallBack.fileProgress ~uri ~version d
let perfData ~io ~uri ~version pd = io.CallBack.perfData ~uri ~version pd
let serverVersion ~io vi = io.CallBack.serverVersion vi
let serverStatus ~io st = io.CallBack.serverStatus st
let execInfo ~io ~uri ~version ~range =
io.CallBack.execInfo ~uri ~version ~range
end