open Pxp_types;;
open Pxp_yacc;;
-let debug = true;;
+let debug = 2;; (* 0 -> no debug
+ 1 -> waiting for an answer / answer received
+ 2 -> XML messages dumping
+ *)
exception Attribute_not_found of string;;
+exception Empty_node;; (** found a node with no _element_ children *)
exception No_element_found of string;;
exception Parse_error of string * string;; (* parsing subject, reason *)
exception Unexpected_message of message;;
| Value s -> s
| _ -> raise Not_found)
with Not_found -> raise (Attribute_not_found name)
+let assert_element n name =
+ match n#node_type with
+ | T_element n when n = name ->
+ ()
+ | _ -> raise (Parse_error ("", "Expected node: " ^ name))
(** given a string representation of a proof asistant state (e.g. the first
child of the XML root of a State_change or Start_musing message), build from
it an HBugs view of a proof assistant state *)
let parse_state (root: ('a node extension as 'a) node) =
- let assert_element n name =
- match n#node_type with
- | T_element n when n = name ->
- ()
- | _ -> raise (Parse_error ("", "Expected node: " ^ name))
- in
+ if (List.filter is_xml_element root#sub_nodes) = [] then
+ raise Empty_node;
let buf = Buffer.create 10240 in
let node_to_string (node: ('a node extension as 'a) node) =
Buffer.clear buf;
let (goal_node, type_node, body_node) =
try
(find_element "CurrentGoal" root,
- find_element "ConstantType" root, (* TODO e' sempre ConstantType? *)
+ find_element "ConstantType" root,
find_element "CurrentProof" root)
with Not_found ->
raise (Parse_error ("", "Malformed HBugs status XML document"))
in
assert_element root "gTopLevelStatus";
assert_element goal_node "CurrentGoal";
- assert_element type_node "ConstantType"; (* TODO: tutti gli xml 'type' hanno
- come root element "ConstantType"? *)
+ assert_element type_node "ConstantType";
assert_element body_node "CurrentProof";
goal_node#write (`Out_buffer buf) `Enc_utf8;
let (type_string, body_string) =
State_change
(get_attr root "id",
match state_node with
- | Some n ->
- if n#sub_nodes = [] then (* TODO don't trust all sub_nodes,
- consider only element sub_nodes *)
- None
- else
- Some (parse_state n)
+ | Some n -> (try Some (parse_state n) with Empty_node -> None)
| None -> None)
| T_element "wow" -> Wow (get_attr root "id")
(* debugging function that dump on stderr the sent messages *)
let dump_msg msg =
- if debug then
+ if debug >= 2 then
prerr_endline
(sprintf "<SENDING_MESSAGE>\n%s\n</SENDING_MESSAGE>"
(match msg with
let submit_req ~url msg =
dump_msg msg;
- if debug then (prerr_string "Waiting for an answer ... "; flush stderr);
+ if debug >= 1 then (prerr_string "Waiting for an answer ... "; flush stderr);
let res =
msg_of_string (Hbugs_misc.http_post ~body:(string_of_msg msg) url)
in
- if debug then (prerr_string "answer received!\n"; flush stderr);
+ if debug >= 1 then (prerr_string "answer received!\n"; flush stderr);
res
;;
let return_xml_msg body outchan =