1 exception IllFormedXml of int;;
3 (* Utility functions that transform a Pxp attribute into something useful *)
6 let module T = Pxp_types in
9 | _ -> raise (IllFormedXml 0)
12 exception DontKnowWhatToDo;;
14 let rec string_of_annotations n =
15 let module D = Pxp_document in
16 let module T = Pxp_types in
17 match n#node_type with
22 match n#attribute att with
23 T.Value s -> " " ^ att ^ "=\"" ^ s ^ "\"" ^ i
24 | T.Implied_value -> i
25 | T.Valuelist l -> " " ^ att ^ "=\"" ^ String.concat " " l ^ "\"" ^ i
26 ) (n#attribute_names) "" ^
27 (match n#sub_nodes with
31 String.concat "" (List.map string_of_annotations l) ^
35 | _ -> raise DontKnowWhatToDo
38 let get_annotation n =
39 String.concat "" (List.map string_of_annotations (n#sub_nodes))
42 let annotate_object ann obj =
46 C.ADefinition (_, rann, _, _, _, _) -> rann
47 | C.AAxiom (_, rann, _, _, _) -> rann
48 | C.AVariable (_, rann, _, _) -> rann
49 | C.ACurrentProof (_, rann, _, _, _, _) -> rann
50 | C.AInductiveDefinition (_, rann, _, _, _) -> rann
55 let annotate_term ann term =
59 C.ARel (_, rann, _, _) -> rann
60 | C.AVar (_, rann, _) -> rann
61 | C.AMeta (_, rann, _) -> rann
62 | C.ASort (_, rann, _) -> rann
63 | C.AImplicit (_, rann) -> rann
64 | C.ACast (_, rann, _, _) -> rann
65 | C.AProd (_, rann, _, _, _) -> rann
66 | C.ALambda (_, rann, _, _, _) -> rann
67 | C.AAppl (_, rann, _) -> rann
68 | C.AConst (_, rann, _, _) -> rann
69 | C.AAbst (_, rann, _) -> rann
70 | C.AMutInd (_, rann, _, _, _) -> rann
71 | C.AMutConstruct (_, rann, _, _, _, _) -> rann
72 | C.AMutCase (_, rann, _, _, _, _, _, _) -> rann
73 | C.AFix (_, rann, _, _) -> rann
74 | C.ACoFix (_, rann, _, _) -> rann
79 let annotate ids_to_targets n =
80 let module D = Pxp_document in
83 let ntype = n # node_type in
85 D.T_element "Annotation" ->
86 let of_uri = string_of_attr (n # attribute "of") in
89 match Hashtbl.find ids_to_targets of_uri with
90 C.Object o -> annotate_object (get_annotation n) o
91 | C.Term t -> annotate_term (get_annotation n) t
93 Not_found -> assert false
95 | D.T_element _ | D.T_data ->
96 raise (IllFormedXml 1)
97 | _ -> raise DontKnowWhatToDo
99 match n # node_type with
100 D.T_element "Annotations" ->
101 List.iter annotate_elem (n # sub_nodes)
102 | _ -> raise (IllFormedXml 2)