From: Claudio Sacerdoti Coen Date: Tue, 10 Feb 2004 14:03:33 +0000 (+0000) Subject: Bug fixed: when an axiom was asked, an exception was raised (since the X-Git-Tag: V_0_3_0~36 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=768205685b87c4ae4c062b3bc9fa5e51951b2608;p=helm.git Bug fixed: when an axiom was asked, an exception was raised (since the check for an existent body was skipped). --- diff --git a/helm/ocaml/cic_cache/cicCache.ml b/helm/ocaml/cic_cache/cicCache.ml index 394f9db77..29d6a9a2f 100644 --- a/helm/ocaml/cic_cache/cicCache.ml +++ b/helm/ocaml/cic_cache/cicCache.ml @@ -45,12 +45,21 @@ let get_annobj uri = Unix.unlink cicfilename ; annobj | Some bodyuri -> - let cicbodyfilename = G.getxml (U.cicuri_of_uri bodyuri) in + 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 (Some cicbodyfilename) + CicParser.annobj_of_xml cicfilename cicbodyfilename in Unix.unlink cicfilename ; - Unix.unlink cicbodyfilename ; + (match cicbodyfilename with None -> () | Some f -> Unix.unlink f) ; annobj ;; @@ -64,9 +73,18 @@ let get_obj uri = Unix.unlink cicfilename ; obj | Some bodyuri -> - let cicbodyfilename = G.getxml (U.cicuri_of_uri bodyuri) in - let obj = CicParser.obj_of_xml cicfilename (Some cicbodyfilename) in + 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 ; - Unix.unlink cicbodyfilename ; + (match cicbodyfilename with None -> () | Some f -> Unix.unlink f) ; obj ;;