(*
* Copyright (C) 2003, HELM Team.
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
* Department, University of Bologna, Italy.
*
* HELM is free software; you can redistribute it and/or
* modify it under the terms of the GNU General Public License
* as published by the Free Software Foundation; either version 2
* of the License, or (at your option) any later version.
*
* HELM is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with HELM; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston,
* MA 02111-1307, USA.
*
* For details, see the HELM World-Wide-Web page,
* http://cs.unibo.it/helm/.
*)
open Hbugs_types;;
open Printf;;
open Pxp_document;;
open Pxp_types;;
open Pxp_yacc;;
exception Attribute_not_found of string;;
exception No_element_found of string;;
exception Parse_error of string * string;; (* parsing subject, reason *)
let is_xml_element n = match n#node_type with T_element _ -> true | _ -> false
let get_attr node name =
try
(match node#attribute name with
| Value s -> s
| _ -> raise Not_found)
with Not_found -> raise (Attribute_not_found name)
let parse_state s = s (* TODO parsare lo stato del proof assistant! *)
let parse_hint s = s (* TODO parsare il possibile suggerimento *)
let parse_hint_type n = n#data (* TODO parsare il possibile tipo di suggerimento *)
let parse_tutor_dscs n =
List.map
(fun n -> (get_attr n "id", n#data))
(List.filter is_xml_element n#sub_nodes)
let parse_tutor_ids node =
List.map
(fun n -> get_attr n "id") (List.filter is_xml_element node#sub_nodes)
let tutors_sep = Pcre.regexp ",\\s*"
let msg_of_string' s =
let root = (* xml tree's root *)
parse_wfcontent_entity default_config (from_string s) default_spec
in
match root#node_type with
(* general purpose *)
| T_element "exception" -> Exception (get_attr root "name", root#data)
(* client -> broker *)
| T_element "register_client" ->
Register_client (get_attr root "id", get_attr root "url")
| T_element "unregister_client" -> Unregister_client (get_attr root "id")
| T_element "list_tutors" -> List_tutors (get_attr root "id")
| T_element "subscribe" ->
Subscribe (get_attr root "id", parse_tutor_ids root)
| T_element "state_change" ->
State_change (get_attr root "id", parse_state root#data)
(* tutor -> broker *)
| T_element "register_tutor" ->
let hint_node = find_element "hint_type" root in
let dsc_node = find_element "description" root in
Register_tutor
(get_attr root "id", get_attr root "url",
parse_hint_type hint_node, dsc_node#data)
| T_element "unregister_tutor" -> Unregister_tutor (get_attr root "id")
| T_element "musing_started" ->
Musing_started (get_attr root "id", get_attr root "musing_id")
| T_element "musing_aborted" ->
Musing_started (get_attr root "id", get_attr root "musing_id")
| T_element "musing_completed" ->
let main_node =
try
find_element "eureka" root
with Not_found -> find_element "sorry" root
in
Musing_completed
(get_attr root "id", get_attr root "musing_id",
(match main_node#node_type with
| T_element "eureka" -> Eureka main_node#data (* TODO come parsare sta roba? *)
| T_element "sorry" -> Sorry
| _ -> assert false)) (* can't be there, see 'find_element' above *)
(* broker -> client *)
| T_element "client_registered" -> Client_registered (get_attr root "id")
| T_element "client_unregistered" -> Client_unregistered (get_attr root "id")
| T_element "tutor_list" ->
Tutor_list (get_attr root "id", parse_tutor_dscs root)
| T_element "subscribed" ->
Subscribed (get_attr root "id", parse_tutor_ids root)
| T_element "state_accepted" ->
State_accepted
(get_attr root "id",
List.map
(fun n -> get_attr n "id")
(List.filter is_xml_element (find_element "stopped" root)#sub_nodes),
List.map
(fun n -> get_attr n "id")
(List.filter is_xml_element (find_element "started" root)#sub_nodes))
| T_element "hint" -> Hint (get_attr root "id", parse_hint root#data)
(* broker -> tutor *)
| T_element "tutor_registered" -> Tutor_registered (get_attr root "id")
| T_element "tutor_unregistered" -> Tutor_unregistered (get_attr root "id")
| T_element "start_musing" ->
Start_musing (get_attr root "id", parse_state root#data)
| T_element "abort_musing" ->
Abort_musing (get_attr root "id", get_attr root "musing_id")
| T_element "thanks" -> Thanks (get_attr root "id", get_attr root "musing_id")
| _ -> raise (No_element_found s)
let msg_of_string s =
try
msg_of_string' s
with e -> raise (Parse_error (s, Printexc.to_string e))
let pp_state s = s (* TODO pretty print state *)
let pp_hint s = s (* TODO pretty print hint *)
let pp_hint_type s = s (* TODO pretty print hint_type *)
let pp_tutor_dscs =
List.fold_left
(fun s (id, dsc) ->
sprintf "%s%s" s id dsc)
""
let pp_tutor_ids =
List.fold_left (fun s id -> sprintf "%s" s id) ""
let string_of_msg = function
| Exception (name, value) ->
sprintf "%s" name value
| Register_client (id, url) ->
sprintf "" id url
| Unregister_client id -> sprintf "" id
| List_tutors id -> sprintf "" id
| Subscribe (id, tutor_ids) ->
sprintf "%s"
id (pp_tutor_ids tutor_ids)
| State_change (id, state) ->
sprintf "%s"
id (pp_state state)
| Register_tutor (id, url, hint_type, dsc) ->
sprintf
"
%s
%s
"
id url (pp_hint_type hint_type) dsc
| Unregister_tutor id -> sprintf "" id
| Musing_started (id, musing_id) ->
sprintf "" id musing_id
| Musing_aborted (id, musing_id) ->
sprintf "" id musing_id
| Musing_completed (id, musing_id, result) ->
sprintf
"%s"
id musing_id
(match result with
| Sorry -> ""
| Eureka s -> sprintf "%s" s)
| Client_registered id -> sprintf "" id
| Client_unregistered id -> sprintf "" id
| Tutor_list (id, tutor_dscs) ->
sprintf "%s"
id (pp_tutor_dscs tutor_dscs)
| Subscribed (id, tutor_ids) ->
sprintf "%s"
id (pp_tutor_ids tutor_ids)
| State_accepted (id, stop_ids, start_ids) ->
sprintf
"
%s
%s
"
id
(String.concat ""
(List.map (fun id -> sprintf "" id) stop_ids))
(String.concat ""
(List.map (fun id -> sprintf "" id) start_ids))
| Hint (id, hint) -> sprintf "%s" id (pp_hint hint)
| Tutor_registered id -> sprintf "" id
| Tutor_unregistered id -> sprintf "" id
| Start_musing (id, state) ->
sprintf "%s" id (pp_state state)
| Abort_musing (id, musing_id) ->
sprintf "" id musing_id
| Thanks (id, musing_id) ->
sprintf "" id musing_id