let module G = Getter in
let module U = UriManager in
let cicfilename = G.getxml (U.cicuri_of_uri uri) in
- CicParser.annobj_of_xml cicfilename uri
+ match (U.bodyuri_of_uri uri) with
+ None ->
+ let annobj = CicParser.annobj_of_xml cicfilename None in
+ Unix.unlink cicfilename ;
+ annobj
+ | Some bodyuri ->
+ let cicbodyfilename =
+ try
+ ignore (Getter.resolve bodyuri) ;
+ (* The body exists ==> it is not an axiom *)
+ Some (Getter.getxml bodyuri)
+ with
+ Getter.Unresolved ->
+ (* The body does not exist ==> we consider it an axiom *)
+ None
+ in
+ let annobj =
+ CicParser.annobj_of_xml cicfilename cicbodyfilename
+ in
+ Unix.unlink cicfilename ;
+ (match cicbodyfilename with None -> () | Some f -> Unix.unlink f) ;
+ annobj
;;
let get_obj uri =
let module G = Getter in
let module U = UriManager in
let cicfilename = G.getxml (U.cicuri_of_uri uri) in
- CicParser.obj_of_xml cicfilename uri
+ match (U.bodyuri_of_uri uri) with
+ None ->
+ let obj = CicParser.obj_of_xml cicfilename None in
+ Unix.unlink cicfilename ;
+ obj
+ | Some bodyuri ->
+ let cicbodyfilename =
+ try
+ ignore (Getter.resolve bodyuri) ;
+ (* The body exists ==> it is not an axiom *)
+ Some (Getter.getxml bodyuri)
+ with
+ Getter.Unresolved ->
+ (* The body does not exist ==> we consider it an axiom *)
+ None
+ in
+ let obj = CicParser.obj_of_xml cicfilename cicbodyfilename in
+ Unix.unlink cicfilename ;
+ (match cicbodyfilename with None -> () | Some f -> Unix.unlink f) ;
+ obj
;;