]> matita.cs.unibo.it Git - helm.git/blob - helm/hbugs/common/hbugs_messages.ml
67e739c603ad5379fe557175fbcd98b936e156f9
[helm.git] / helm / hbugs / common / hbugs_messages.ml
1 (*
2  *  Copyright (C) 2003, HELM Team.
3  *
4  *  This file is part of HELM, an Hypertextual, Electronic
5  *  Library of Mathematics, developed at the Computer Science
6  *  Department, University of Bologna, Italy.
7  *
8  *  HELM is free software; you can redistribute it and/or
9  *  modify it under the terms of the GNU General Public License
10  *  as published by the Free Software Foundation; either version 2
11  *  of the License, or (at your option) any later version.
12  *
13  *  HELM is distributed in the hope that it will be useful,
14  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
15  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
16  *  GNU General Public License for more details.
17  *
18  *  You should have received a copy of the GNU General Public License
19  *  along with HELM; if not, write to the Free Software
20  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
21  *  MA  02111-1307, USA.
22  *
23  *  For details, see the HELM World-Wide-Web page,
24  *  http://cs.unibo.it/helm/.
25  *)
26
27 open Hbugs_types;;
28 open Printf;;
29 open Pxp_document;;
30 open Pxp_types;;
31 open Pxp_yacc;;
32
33 exception Attribute_not_found of string;;
34 exception No_element_found of string;;
35 exception Parse_error of string * string;;  (* parsing subject, reason *)
36
37 let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
38 let get_attr node name =
39   try
40     (match node#attribute name with
41     | Value s -> s
42     | _ -> raise Not_found)
43   with Not_found -> raise (Attribute_not_found name)
44
45 let parse_state s = s (* TODO parsare lo stato del proof assistant! *)
46 let parse_hint s = s (* TODO parsare il possibile suggerimento *)
47 let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
48 let parse_tutor_dscs n =
49   List.map
50     (fun n -> (get_attr n "id", n#data))
51     (List.filter is_xml_element n#sub_nodes)
52 let parse_tutor_ids node =
53   List.map
54     (fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
55
56 let tutors_sep = Pcre.regexp ",\\s*"
57
58 let msg_of_string' s =
59   let root =  (* xml tree's root *)
60     parse_wfcontent_entity default_config (from_string s) default_spec
61   in
62   match root#node_type with
63
64     (* general purpose *)
65   | T_element "exception" -> Exception (get_attr root "name", root#data)
66
67     (* client -> broker *)
68   | T_element "register_client" ->
69       Register_client (get_attr root "id", get_attr root "url")
70   | T_element "unregister_client" -> Unregister_client (get_attr root "id")
71   | T_element "list_tutors" -> List_tutors (get_attr root "id")
72   | T_element "subscribe" ->
73       Subscribe (get_attr root "id", parse_tutor_ids root)
74   | T_element "state_change" ->
75       State_change (get_attr root "id", parse_state root#data)
76
77     (* tutor -> broker *)
78   | T_element "register_tutor" ->
79       let hint_node = find_element "hint_type" root in
80       let dsc_node = find_element "description" root in
81       Register_tutor
82         (get_attr root "id", get_attr root "url",
83         parse_hint_type hint_node, dsc_node#data)
84   | T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
85   | T_element "musing_started" ->
86       Musing_started (get_attr root "id", get_attr root "musing_id")
87   | T_element "musing_aborted" ->
88       Musing_started (get_attr root "id", get_attr root "musing_id")
89   | T_element "musing_completed" ->
90       let main_node =
91         try
92           find_element "eureka" root
93         with Not_found -> find_element "sorry" root
94       in
95       Musing_completed
96         (get_attr root "id", get_attr root "musing_id",
97         (match main_node#node_type with
98         | T_element "eureka" -> Eureka main_node#data (* TODO come parsare sta roba? *)
99         | T_element "sorry" -> Sorry
100         | _ -> assert false)) (* can't be there, see 'find_element' above *)
101
102     (* broker -> client *)
103   | T_element "client_registered" -> Client_registered (get_attr root "id")
104   | T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
105   | T_element "tutor_list" ->
106       Tutor_list (get_attr root "id", parse_tutor_dscs root)
107   | T_element "subscribed" ->
108       Subscribed (get_attr root "id", parse_tutor_ids root)
109   | T_element "state_accepted" ->
110       State_accepted
111         (get_attr root "id",
112         List.map
113           (fun n -> get_attr n "id")
114           (List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
115         List.map
116           (fun n -> get_attr n "id")
117           (List.filter is_xml_element (find_element "started" root)#sub_nodes))
118   | T_element "hint" -> Hint (get_attr root "id", parse_hint root#data)
119
120     (* broker -> tutor *)
121   | T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
122   | T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
123   | T_element "start_musing" ->
124       Start_musing (get_attr root "id", parse_state root#data)
125   | T_element "abort_musing" ->
126       Abort_musing (get_attr root "id", get_attr root "musing_id")
127   | T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
128
129   | _ -> raise (No_element_found s)
130
131 let msg_of_string s =
132   try
133     msg_of_string' s
134   with e -> raise (Parse_error (s, Printexc.to_string e))
135
136 let pp_state s = s  (* TODO pretty print state *)
137 let pp_hint s = s   (* TODO pretty print hint *)
138 let pp_hint_type s = s   (* TODO pretty print hint_type *)
139 let pp_tutor_dscs =
140   List.fold_left
141     (fun s (id, dsc) ->
142       sprintf "%s<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
143     ""
144 let pp_tutor_ids =
145   List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
146
147 let string_of_msg = function
148   | Exception (name, value) ->
149       sprintf "<exception name=\"%s\">%s</exception>" name value
150   | Register_client (id, url) ->
151       sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
152   | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
153   | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
154   | Subscribe (id, tutor_ids) ->
155       sprintf "<subscribe id=\"%s\">%s</subscribe>"
156         id (pp_tutor_ids tutor_ids)
157   | State_change (id, state) ->
158       sprintf "<state_change id=\"%s\">%s</state_change>"
159         id (pp_state state)
160   | Register_tutor (id, url, hint_type, dsc) ->
161       sprintf
162 "<register_tutor id=\"%s\" url=\"%s\">
163 <hint_type>%s</hint_type>
164 <description>%s</description>
165 </register_tutor>"
166         id url (pp_hint_type hint_type) dsc
167   | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
168   | Musing_started (id, musing_id) ->
169       sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
170   | Musing_aborted (id, musing_id) ->
171       sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
172   | Musing_completed (id, musing_id, result) ->
173       sprintf
174         "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
175         id musing_id
176         (match result with
177         | Sorry -> "<sorry />"
178         | Eureka s -> sprintf "<eureka>%s</eureka>" s)
179   | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
180   | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
181   | Tutor_list (id, tutor_dscs) ->
182       sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
183         id (pp_tutor_dscs tutor_dscs)
184   | Subscribed (id, tutor_ids) ->
185       sprintf "<subscribed id=\"%s\">%s</subscribed>"
186         id (pp_tutor_ids tutor_ids)
187   | State_accepted (id, stop_ids, start_ids) ->
188       sprintf
189 "<state_accepted id=\"%s\">
190 <stopped>%s</stopped>
191 <started>%s</started>
192 </state_accepted>"
193         id
194         (String.concat ""
195           (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
196         (String.concat ""
197           (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
198   | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
199   | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
200   | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
201   | Start_musing (id, state) ->
202       sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
203   | Abort_musing (id, musing_id) ->
204       sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
205   | Thanks (id, musing_id) ->
206       sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
207