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
|
(************************************************************************)
(* 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
open Serialize
type message_level =
| Debug of string
| Info
| Notice
| Warning
| Error
type message = {
message_level : message_level;
message_content : string;
}
let of_message_level = function
| Debug s ->
Serialize.constructor "message_level" "debug" [Xml_datatype.PCData s]
| Info -> Serialize.constructor "message_level" "info" []
| Notice -> Serialize.constructor "message_level" "notice" []
| Warning -> Serialize.constructor "message_level" "warning" []
| Error -> Serialize.constructor "message_level" "error" []
let to_message_level =
Serialize.do_match "message_level" (fun s args -> match s with
| "debug" -> Debug (Serialize.raw_string args)
| "info" -> Info
| "notice" -> Notice
| "warning" -> Warning
| "error" -> Error
| _ -> raise Serialize.Marshal_error)
let of_message msg =
let lvl = of_message_level msg.message_level in
let content = Serialize.of_string msg.message_content in
Xml_datatype.Element ("message", [], [lvl; content])
let to_message xml = match xml with
| Xml_datatype.Element ("message", [], [lvl; content]) -> {
message_level = to_message_level lvl;
message_content = Serialize.to_string content }
| _ -> raise Serialize.Marshal_error
let is_message = function
| Xml_datatype.Element ("message", _, _) -> true
| _ -> false
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
| ErrorMsg of Loc.t * string
| 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
| Custom of Loc.t * string * xml
| Message of message
type feedback = {
id : edit_or_state_id;
contents : feedback_content;
route : route_id;
}
let to_feedback_content = do_match "feedback_content" (fun s a -> match s,a with
| "addedaxiom", _ -> AddedAxiom
| "processed", _ -> Processed
| "processingin", [where] -> ProcessingIn (to_string where)
| "incomplete", _ -> Incomplete
| "complete", _ -> Complete
| "globref", [loc; filepath; modpath; ident; ty] ->
GlobRef(to_loc loc, to_string filepath,
to_string modpath, to_string ident, to_string ty)
| "globdef", [loc; ident; secpath; ty] ->
GlobDef(to_loc loc, to_string ident, to_string secpath, to_string ty)
| "errormsg", [loc; s] -> ErrorMsg (to_loc loc, to_string s)
| "inprogress", [n] -> InProgress (to_int n)
| "workerstatus", [ns] ->
let n, s = to_pair to_string to_string ns in
WorkerStatus(n,s)
| "goals", [loc;s] -> Goals (to_loc loc, to_string s)
| "custom", [loc;name;x]-> Custom (to_loc loc, to_string name, x)
| "filedependency", [from; dep] ->
FileDependency (to_option to_string from, to_string dep)
| "fileloaded", [dirpath; filename] ->
FileLoaded (to_string dirpath, to_string filename)
| "message", [m] -> Message (to_message m)
| _ -> raise Marshal_error)
let of_feedback_content = function
| AddedAxiom -> constructor "feedback_content" "addedaxiom" []
| Processed -> constructor "feedback_content" "processed" []
| ProcessingIn where ->
constructor "feedback_content" "processingin" [of_string where]
| Incomplete -> constructor "feedback_content" "incomplete" []
| Complete -> constructor "feedback_content" "complete" []
| GlobRef(loc, filepath, modpath, ident, ty) ->
constructor "feedback_content" "globref" [
of_loc loc;
of_string filepath;
of_string modpath;
of_string ident;
of_string ty ]
| GlobDef(loc, ident, secpath, ty) ->
constructor "feedback_content" "globdef" [
of_loc loc;
of_string ident;
of_string secpath;
of_string ty ]
| ErrorMsg(loc, s) ->
constructor "feedback_content" "errormsg" [of_loc loc; of_string s]
| InProgress n -> constructor "feedback_content" "inprogress" [of_int n]
| WorkerStatus(n,s) ->
constructor "feedback_content" "workerstatus"
[of_pair of_string of_string (n,s)]
| Goals (loc,s) ->
constructor "feedback_content" "goals" [of_loc loc;of_string s]
| Custom (loc, name, x) ->
constructor "feedback_content" "custom" [of_loc loc; of_string name; x]
| FileDependency (from, depends_on) ->
constructor "feedback_content" "filedependency" [
of_option of_string from;
of_string depends_on]
| FileLoaded (dirpath, filename) ->
constructor "feedback_content" "fileloaded" [
of_string dirpath;
of_string filename ]
| Message m -> constructor "feedback_content" "message" [ of_message m ]
let of_edit_or_state_id = function
| Edit id -> ["object","edit"], of_edit_id id
| State id -> ["object","state"], Stateid.to_xml id
let of_feedback msg =
let content = of_feedback_content msg.contents in
let obj, id = of_edit_or_state_id msg.id in
let route = string_of_int msg.route in
Element ("feedback", obj @ ["route",route], [id;content])
let to_feedback xml = match xml with
| Element ("feedback", ["object","edit";"route",route], [id;content]) -> {
id = Edit(to_edit_id id);
route = int_of_string route;
contents = to_feedback_content content }
| Element ("feedback", ["object","state";"route",route], [id;content]) -> {
id = State(Stateid.of_xml id);
route = int_of_string route;
contents = to_feedback_content content }
| _ -> raise Marshal_error
let is_feedback = function
| Element ("feedback", _, _) -> true
| _ -> false
let default_route = 0
|
