(* * Copyright (C) 2003: * Stefano Zacchiroli * for the HELM Team http://helm.cs.unibo.it/ * * 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://helm.cs.unibo.it/ *) 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 "help" -> Help | T_element "usage" -> Usage root#data | 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 | Help -> "" | Usage usage_string -> sprintf "%s" usage_string | 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 let submit_req ~url msg = msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url) let return_xml_msg body outchan = Http_daemon.respond ~headers:["Content-Type", "text/xml"] ~body outchan let respond_msg msg = return_xml_msg (string_of_msg msg);; let respond_exc name value = respond_msg (Exception (name, value));;