exception No_element_found of string;;
exception Parse_error of string * string;; (* parsing subject, reason *)
exception Unexpected_message of message;;
exception No_element_found of string;;
exception Parse_error of string * string;; (* parsing subject, reason *)
exception Unexpected_message of message;;
(** 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) =
(** 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 (goal_node, type_node, body_node) =
try
(find_element "CurrentGoal" root,
let (goal_node, type_node, body_node) =
try
(find_element "CurrentGoal" 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";
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 body_node "CurrentProof";
goal_node#write (`Out_buffer buf) `Enc_utf8;
let (type_string, body_string) =
assert_element body_node "CurrentProof";
goal_node#write (`Out_buffer buf) `Enc_utf8;
let (type_string, body_string) =
| 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")
| 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")
-let pp_state (type_string, body_string, goal) =
- (* ASSUMPTION: type_string and body_string are well formed XML document
- contents (i.e. they don't contain heading <?xml ... ?> declaration nor DOCTYPE
- one *)
- let res =
+let pp_state = function
+ | Some (type_string, body_string, goal) ->
+ (* ASSUMPTION: type_string and body_string are well formed XML document
+ contents (i.e. they don't contain heading <?xml ... ?> declaration nor
+ DOCTYPE one *)
| Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
| Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
| Start_musing (id, state) ->
| Tutor_registered id -> sprintf "<tutor_registered id=\"%s\" />" id
| Tutor_unregistered id -> sprintf "<tutor_unregistered id=\"%s\" />" id
| Start_musing (id, state) ->
| Abort_musing (id, musing_id) ->
sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
| Thanks (id, musing_id) ->
| Abort_musing (id, musing_id) ->
sprintf "<abort_musing id=\"%s\" musing_id=\"%s\" />" id musing_id
| Thanks (id, musing_id) ->