From 768205685b87c4ae4c062b3bc9fa5e51951b2608 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 10 Feb 2004 14:03:33 +0000 Subject: [PATCH] Bug fixed: when an axiom was asked, an exception was raised (since the check for an existent body was skipped). --- helm/ocaml/cic_cache/cicCache.ml | 30 ++++++++++++++++++++++++------ 1 file changed, 24 insertions(+), 6 deletions(-) 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 ;; -- 2.39.2