+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) =
+ 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;
+ node#write (`Out_buffer buf) `Enc_utf8;
+ let res = Buffer.contents buf in
+ Buffer.clear buf;
+ res
+ in
+ let (goal_node, type_node, body_node) =
+ try
+ (find_element "CurrentGoal" root,
+ 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";
+ assert_element body_node "CurrentProof";
+ goal_node#write (`Out_buffer buf) `Enc_utf8;
+ let (type_string, body_string) =
+ (node_to_string type_node, node_to_string body_node)
+ in
+ let goal =
+ try
+ int_of_string (goal_node#data)
+ with Failure "int_of_string" ->
+ raise (Parse_error (goal_node#data, "can't parse goal"))
+ in
+ (type_string, body_string, goal)
+
+ (** parse an hint from an XML node, XML node should have type 'T_element _'
+ (the name is ignored), attributes on it are ignored *)
+let parse_hint node =
+ let rec parse_hint_node node =
+ match node#node_type with
+ | T_element "ring" -> Use_ring_Luke
+ | T_element "fourier" -> Use_fourier_Luke
+ | T_element "reflexivity" -> Use_reflexivity_Luke
+ | T_element "symmetry" -> Use_symmetry_Luke
+ | T_element "assumption" -> Use_assumption_Luke
+ | T_element "contradiction" -> Use_contradiction_Luke
+ | T_element "exists" -> Use_exists_Luke
+ | T_element "split" -> Use_split_Luke
+ | T_element "left" -> Use_left_Luke
+ | T_element "right" -> Use_right_Luke
+ | T_element "apply" -> Use_apply_Luke node#data
+ | T_element "hints" ->
+ Hints
+ (List.map parse_hint_node (List.filter is_xml_element node#sub_nodes))
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)
+ in
+ match List.filter is_xml_element node#sub_nodes with
+ [node] -> parse_hint_node node
+ | _ -> assert false (* CSC: should this assert false be a raise something? *)