--- /dev/null
+(*
+ * 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<tutor_dsc id=\"%s\">%s</tutor_dsc>" s id dsc)
+ ""
+let pp_tutor_ids =
+ List.fold_left (fun s id -> sprintf "%s<tutor id=\"%s\" />" s id) ""
+
+let string_of_msg = function
+ | Exception (name, value) ->
+ sprintf "<exception name=\"%s\">%s</exception>" name value
+ | Register_client (id, url) ->
+ sprintf "<register_client id=\"%s\" url=\"%s\" />" id url
+ | Unregister_client id -> sprintf "<unregister_client id=\"%s\" />" id
+ | List_tutors id -> sprintf "<list_tutors id=\"%s\" />" id
+ | Subscribe (id, tutor_ids) ->
+ sprintf "<subscribe id=\"%s\">%s</subscribe>"
+ id (pp_tutor_ids tutor_ids)
+ | State_change (id, state) ->
+ sprintf "<state_change id=\"%s\">%s</state_change>"
+ id (pp_state state)
+ | Register_tutor (id, url, hint_type, dsc) ->
+ sprintf
+"<register_tutor id=\"%s\" url=\"%s\">
+<hint_type>%s</hint_type>
+<description>%s</description>
+</register_tutor>"
+ id url (pp_hint_type hint_type) dsc
+ | Unregister_tutor id -> sprintf "<unregister_tutor id=\"%s\" />" id
+ | Musing_started (id, musing_id) ->
+ sprintf "<musing_started id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Musing_aborted (id, musing_id) ->
+ sprintf "<musing_aborted id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Musing_completed (id, musing_id, result) ->
+ sprintf
+ "<musing_completed id=\"%s\" musing_id=\"%s\">%s</musing_completed>"
+ id musing_id
+ (match result with
+ | Sorry -> "<sorry />"
+ | Eureka s -> sprintf "<eureka>%s</eureka>" s)
+ | Client_registered id -> sprintf "<client_registered id=\"%s\" />" id
+ | Client_unregistered id -> sprintf "<client_unregistered id=\"%s\" />" id
+ | Tutor_list (id, tutor_dscs) ->
+ sprintf "<tutor_list id=\"%s\">%s</tutor_list>"
+ id (pp_tutor_dscs tutor_dscs)
+ | Subscribed (id, tutor_ids) ->
+ sprintf "<subscribed id=\"%s\">%s</subscribed>"
+ id (pp_tutor_ids tutor_ids)
+ | State_accepted (id, stop_ids, start_ids) ->
+ sprintf
+"<state_accepted id=\"%s\">
+<stopped>%s</stopped>
+<started>%s</started>
+</state_accepted>"
+ id
+ (String.concat ""
+ (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) stop_ids))
+ (String.concat ""
+ (List.map (fun id -> sprintf "<musing id=\"%s\" />" id) start_ids))
+ | Hint (id, hint) -> sprintf "<hint id=\"%s\">%s</hint>" id (pp_hint hint)
+ | Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
+ | Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
+ | Start_musing (id, state) ->
+ sprintf "<start_musing id=\"%s\">%s</start_musing>" id (pp_state state)
+ | Abort_musing (id, musing_id) ->
+ sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
+ | Thanks (id, musing_id) ->
+ sprintf "<thanks id=\"%s\" musing_id=\"%s\" />" id musing_id
+
projects / helm.git / blobdiff