exception IllFormedXml of int;; (* Utility functions that transform a Pxp attribute into something useful *) let string_of_attr a = let module T = Pxp_types in match a with T.Value s -> s | _ -> raise (IllFormedXml 0) let get_theory n = let module D = Pxp_document in let module T = Theory in let rec get_theory_elem n = let ntype = n # node_type in match ntype with D.T_element "THEOREM" -> let uri = string_of_attr (n # attribute "uri") in T.Theorem uri | D.T_element "DEFINITION" -> let uri = string_of_attr (n # attribute "uri") in T.Definition uri | D.T_element "AXIOM" -> let uri = string_of_attr (n # attribute "uri") in T.Axiom uri | D.T_element "VARIABLE" -> let uri = string_of_attr (n # attribute "uri") in T.Variable uri | D.T_element "SECTION" -> let uri = string_of_attr (n # attribute "uri") and subtheory = List.map get_theory_elem (n # sub_nodes) in T.Section (uri, subtheory) | D.T_element _ | D.T_data | _ -> raise (IllFormedXml 1) in match n # node_type with D.T_element "Theory" -> let uri = string_of_attr (n # attribute "uri") in (uri, List.map get_theory_elem (n # sub_nodes)) | _ -> raise (IllFormedXml 2) ;;