- let filename = Http_getter.getxml' uri in
- let bodyfilename =
- match UriManager.bodyuri_of_uri uri with
- None -> None
- | Some bodyuri ->
- try
- ignore (Http_getter.resolve' bodyuri) ;
- (* The body exists ==> it is not an axiom *)
- Some (Http_getter.getxml' bodyuri)
- with
- Http_getter_types.Key_not_found _ ->
- (* The body does not exist ==> we consider it an axiom *)
- None
- in
- let cleanup () =
- Unix.unlink filename ;
- (*
- begin
- match filename_univ with
- Some f -> Unix.unlink f
- | None -> ()
- end;
- *)
- begin
- match bodyfilename with
- Some f -> Unix.unlink f
- | None -> ()
- end
- in
- (* this brakes something :
- * let _ = CicUniv.restart_numbering () in
- *)
- let obj =
- try
- CicParser.obj_of_xml filename bodyfilename
- with exn ->
- cleanup ();
- raise exn
- in
+ try
+ let filename = Http_getter.getxml' uri in
+ let bodyfilename =
+ match UriManager.bodyuri_of_uri uri with
+ None -> None
+ | Some bodyuri ->
+ try
+ ignore (Http_getter.resolve' bodyuri) ;
+ (* The body exists ==> it is not an axiom *)
+ Some (Http_getter.getxml' bodyuri)
+ with
+ Http_getter_types.Key_not_found _ ->
+ (* The body does not exist ==> we consider it an axiom *)
+ None
+ in
+ let cleanup () =
+ Unix.unlink filename ;
+ (*
+ begin
+ match filename_univ with
+ Some f -> Unix.unlink f
+ | None -> ()
+ end;
+ *)
+ begin
+ match bodyfilename with
+ Some f -> Unix.unlink f
+ | None -> ()
+ end
+ in
+ (* restarts the numbering of named universes (the ones inside the cic) *)
+ let _ = CicUniv.restart_numbering () in
+ let obj =
+ try
+ let time = Unix.gettimeofday() in
+ let rc = CicParser.obj_of_xml uri filename bodyfilename in
+ total_parsing_time :=
+ !total_parsing_time +. ((Unix.gettimeofday()) -. time );
+ rc
+ with exn ->
+ cleanup ();
+ (match exn with
+ | CicParser.Getter_failure ("key_not_found", uri) ->
+ raise (Object_not_found (UriManager.uri_of_string uri))
+ | _ -> raise exn)
+ in