blob: 4bda936f2b44029db76866d5ca7d795b7e1bec4d (
plain)
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
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
|
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
open Xml_datatype
type level =
| Debug
| Info
| Notice
| Warning
| Error
type edit_id = int
type state_id = Stateid.t
type edit_or_state_id = Edit of edit_id | State of state_id
type route_id = int
type feedback_content =
| Processed
| Incomplete
| Complete
| ProcessingIn of string
| InProgress of int
| WorkerStatus of string * string
| Goals of Loc.t * 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 * string * xml
(* Generic messages *)
| Message of level * Loc.t option * Richpp.richpp
type feedback = {
id : edit_or_state_id;
contents : feedback_content;
route : route_id;
}
let default_route = 0
(** Feedback and logging *)
open Pp
open Pp_control
type logger = ?loc:Loc.t -> level -> std_ppcmds -> unit
let msgnl_with fmt strm = msg_with fmt (strm ++ fnl ())
let msgnl strm = msgnl_with !std_ft strm
(* XXX: This is really painful! *)
module Emacs = struct
(* Special chars for emacs, to detect warnings inside goal output *)
let emacs_quote_start = String.make 1 (Char.chr 254)
let emacs_quote_end = String.make 1 (Char.chr 255)
let emacs_quote_err g =
hov 0 (str emacs_quote_start ++ g ++ str emacs_quote_end)
let emacs_quote_info_start = "<infomsg>"
let emacs_quote_info_end = "</infomsg>"
let emacs_quote_info g =
hov 0 (str emacs_quote_info_start++ brk(0,0) ++ g ++ brk(0,0) ++ str emacs_quote_info_end)
end
open Emacs
let dbg_str = str "Debug:" ++ spc ()
let info_str = mt ()
let warn_str = str "Warning:" ++ spc ()
let err_str = str "Error:" ++ spc ()
let make_body quoter info ?loc s =
let loc = Option.cata Pp.pr_loc (Pp.mt ()) loc in
quoter (hov 0 (loc ++ info ++ s))
(* Generic logger *)
let gen_logger dbg err ?loc level msg = match level with
| Debug -> msgnl (make_body dbg dbg_str ?loc msg)
| Info -> msgnl (make_body dbg info_str ?loc msg)
(* XXX: What to do with loc here? *)
| Notice -> msgnl msg
| Warning -> Flags.if_warn (fun () ->
msgnl_with !err_ft (make_body err warn_str ?loc msg)) ()
| Error -> msgnl_with !err_ft (make_body err err_str ?loc msg)
(** Standard loggers *)
let std_logger = gen_logger (fun x -> x) (fun x -> x)
(* Color logger *)
let color_terminal_logger ?loc level strm =
let msg = Ppstyle.color_msg in
match level with
| Debug -> msg ?loc ~header:("Debug", Ppstyle.debug_tag) !std_ft strm
| Info -> msg ?loc !std_ft strm
| Notice -> msg ?loc !std_ft strm
| Warning -> Flags.if_warn (fun () ->
msg ?loc ~header:("Warning", Ppstyle.warning_tag) !err_ft strm) ()
| Error -> msg ?loc ~header:("Error", Ppstyle.error_tag) !err_ft strm
(* Rules for emacs:
- Debug/info: emacs_quote_info
- Warning/Error: emacs_quote_err
- Notice: unquoted
*)
let emacs_logger = gen_logger emacs_quote_info emacs_quote_err
let logger = ref std_logger
let set_logger l = logger := l
let msg_info ?loc x = !logger ?loc Info x
let msg_notice ?loc x = !logger ?loc Notice x
let msg_warning ?loc x = !logger ?loc Warning x
let msg_error ?loc x = !logger ?loc Error x
let msg_debug ?loc x = !logger ?loc Debug x
(** Feeders *)
let feeders = ref []
let add_feeder f = feeders := f :: !feeders
let feedback_id = ref (Edit 0)
let feedback_route = ref default_route
let set_id_for_feedback ?(route=default_route) i =
feedback_id := i; feedback_route := route
let feedback ?id ?route what =
let m = {
contents = what;
route = Option.default !feedback_route route;
id = Option.default !feedback_id id;
} in
List.iter (fun f -> f m) !feeders
let feedback_logger ?loc lvl msg =
feedback ~route:!feedback_route ~id:!feedback_id
(Message (lvl, loc, Richpp.richpp_of_pp msg))
(* Output to file *)
let ft_logger old_logger ft ?loc level mesg =
let id x = x in
match level with
| Debug -> msgnl_with ft (make_body id dbg_str mesg)
| Info -> msgnl_with ft (make_body id info_str mesg)
| Notice -> msgnl_with ft mesg
| Warning -> old_logger ?loc level mesg
| Error -> old_logger ?loc level mesg
let with_output_to_file fname func input =
let old_logger = !logger in
let channel = open_out (String.concat "." [fname; "out"]) in
logger := ft_logger old_logger (Format.formatter_of_out_channel channel);
try
let output = func input in
logger := old_logger;
close_out channel;
output
with reraise ->
let reraise = Backtrace.add_backtrace reraise in
logger := old_logger;
close_out channel;
Exninfo.iraise reraise
|
