3 * Stefano Zacchiroli <zack@cs.unibo.it>
4 * for the HELM Team http://helm.cs.unibo.it/
6 * This file is part of HELM, an Hypertextual, Electronic
7 * Library of Mathematics, developed at the Computer Science
8 * Department, University of Bologna, Italy.
10 * HELM is free software; you can redistribute it and/or
11 * modify it under the terms of the GNU General Public License
12 * as published by the Free Software Foundation; either version 2
13 * of the License, or (at your option) any later version.
15 * HELM is distributed in the hope that it will be useful,
16 * but WITHOUT ANY WARRANTY; without even the implied warranty of
17 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
18 * GNU General Public License for more details.
20 * You should have received a copy of the GNU General Public License
21 * along with HELM; if not, write to the Free Software
22 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
25 * For details, see the HELM World-Wide-Web page,
26 * http://helm.cs.unibo.it/
35 exception Attribute_not_found of string;;
36 exception No_element_found of string;;
37 exception Parse_error of string * string;; (* parsing subject, reason *)
39 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
40 let get_attr node name =
42 (match node#attribute name with
44 | _ -> raise Not_found)
45 with Not_found -> raise (Attribute_not_found name)
47 let parse_state s = s (* TODO parsare lo stato del proof assistant! *)
48 let parse_hint s = s (* TODO parsare il possibile suggerimento *)
49 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
50 let parse_tutor_dscs n =
52 (fun n -> (get_attr n "id", n#data))
53 (List.filter is_xml_element n#sub_nodes)
54 let parse_tutor_ids node =
56 (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
58 let tutors_sep = Pcre.regexp ",\\s*"
60 let msg_of_string' s =
61 let root = (* xml tree's root *)
62 parse_wfcontent_entity default_config (from_string s) default_spec
64 match root#node_type with
67 | T_element "help" -> Help
68 | T_element "usage" -> Usage root#data
69 | T_element "exception" -> Exception (get_attr root "name", root#data)
71 (* client -> broker *)
72 | T_element "register_client" ->
73 Register_client (get_attr root "id", get_attr root "url")
74 | T_element "unregister_client" -> Unregister_client (get_attr root "id")
75 | T_element "list_tutors" -> List_tutors (get_attr root "id")
76 | T_element "subscribe" ->
77 Subscribe (get_attr root "id", parse_tutor_ids root)
78 | T_element "state_change" ->
79 State_change (get_attr root "id", parse_state root#data)
82 | T_element "register_tutor" ->
83 let hint_node = find_element "hint_type" root in
84 let dsc_node = find_element "description" root in
86 (get_attr root "id", get_attr root "url",
87 parse_hint_type hint_node, dsc_node#data)
88 | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
89 | T_element "musing_started" ->
90 Musing_started (get_attr root "id", get_attr root "musing_id")
91 | T_element "musing_aborted" ->
92 Musing_started (get_attr root "id", get_attr root "musing_id")
93 | T_element "musing_completed" ->
96 find_element "eureka" root
97 with Not_found -> find_element "sorry" root
100 (get_attr root "id", get_attr root "musing_id",
101 (match main_node#node_type with
102 | T_element "eureka" -> Eureka main_node#data (* TODO come parsare sta roba? *)
103 | T_element "sorry" -> Sorry
104 | _ -> assert false)) (* can't be there, see 'find_element' above *)
106 (* broker -> client *)
107 | T_element "client_registered" -> Client_registered (get_attr root "id")
108 | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
109 | T_element "tutor_list" ->
110 Tutor_list (get_attr root "id", parse_tutor_dscs root)
111 | T_element "subscribed" ->
112 Subscribed (get_attr root "id", parse_tutor_ids root)
113 | T_element "state_accepted" ->
117 (fun n -> get_attr n "id")
118 (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
120 (fun n -> get_attr n "id")
121 (List.filter is_xml_element (find_element "started" root)#sub_nodes))
122 | T_element "hint" -> Hint (get_attr root "id", parse_hint root#data)
124 (* broker -> tutor *)
125 | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
126 | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
127 | T_element "start_musing" ->
128 Start_musing (get_attr root "id", parse_state root#data)
129 | T_element "abort_musing" ->
130 Abort_musing (get_attr root "id", get_attr root "musing_id")
131 | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
133 | _ -> raise (No_element_found s)
135 let msg_of_string s =
138 with e -> raise (Parse_error (s, Printexc.to_string e))
140 let pp_state s = s (* TODO pretty print state *)
141 let pp_hint s = s (* TODO pretty print hint *)
142 let pp_hint_type s = s (* TODO pretty print hint_type *)
146 sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
149 List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
151 let string_of_msg = function
153 | Usage usage_string -> sprintf "<usage>%s</usage>" usage_string
154 | Exception (name, value) ->
155 sprintf "<exception name=\"%s\">%s</exception>" name value
156 | Register_client (id, url) ->
157 sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
158 | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
159 | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
160 | Subscribe (id, tutor_ids) ->
161 sprintf "<subscribe id=\"%s\">%s</subscribe>"
162 id (pp_tutor_ids tutor_ids)
163 | State_change (id, state) ->
164 sprintf "<state_change id=\"%s\">%s</state_change>"
166 | Register_tutor (id, url, hint_type, dsc) ->
168 "<register_tutor id=\"%s\" url=\"%s\">
169 <hint_type>%s</hint_type>
170 <description>%s</description>
172 id url (pp_hint_type hint_type) dsc
173 | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
174 | Musing_started (id, musing_id) ->
175 sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
176 | Musing_aborted (id, musing_id) ->
177 sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
178 | Musing_completed (id, musing_id, result) ->
180 "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
183 | Sorry -> "<sorry />"
184 | Eureka s -> sprintf "<eureka>%s</eureka>" s)
185 | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
186 | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
187 | Tutor_list (id, tutor_dscs) ->
188 sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
189 id (pp_tutor_dscs tutor_dscs)
190 | Subscribed (id, tutor_ids) ->
191 sprintf "<subscribed id=\"%s\">%s</subscribed>"
192 id (pp_tutor_ids tutor_ids)
193 | State_accepted (id, stop_ids, start_ids) ->
195 "<state_accepted id=\"%s\">
196 <stopped>%s</stopped>
197 <started>%s</started>
201 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
203 (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
204 | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
205 | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
206 | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
207 | Start_musing (id, state) ->
208 sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
209 | Abort_musing (id, musing_id) ->
210 sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
211 | Thanks (id, musing_id) ->
212 sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
214 let submit_req ~url msg =
215 msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
216 let return_xml_msg body outchan =
217 Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan
218 let respond_msg msg = return_xml_msg (string_of_msg msg);;
219 let respond_exc name value = respond_msg (Exception (name, value));;