with
Not_found ->
let filename = Getter.getxml uri in
- let (annobj,_) = CicParser.term_of_xml filename uri false in
- let obj = Deannotate.deannotate_obj annobj in
- let output = Unchecked obj in
- HashTable.add hashtable (uri,0) output ;
- output
-;;
-
-(* DANGEROUS!!! *)
-(* USEFUL ONLY DURING THE FIXING OF THE FILES *)
-(* change_obj uri (Some newobj) *)
-(* maps uri to newobj in cache. *)
-(* change_obj uri None *)
-(* maps uri to a freeze dummy-object. *)
-let change_obj uri newobj =
- let newobj =
- match newobj with
- Some newobj' -> Unchecked newobj'
- | None -> Frozen (Cic.Variable ("frozen-dummy", None, Cic.Implicit))
- in
- HashTable.remove hashtable (uri,0) ;
- HashTable.add hashtable (uri,0) newobj
+ let obj = CicParser.obj_of_xml filename uri in
+ let output = Unchecked obj in
+ HashTable.add hashtable (uri,0) output ;
+ output
;;
let is_annotation_uri uri =
Str.string_match (Str.regexp ".*\.ann$") (UriManager.string_of_uri uri) 0
;;
-(* returns both the annotated and deannotated uncooked forms (plus the *)
-(* map from ids to annotation targets) *)
-let get_annobj_and_type_checking_info uri =
- let filename = Getter.getxml uri in
- match CicParser.term_of_xml filename uri true with
- (_, None) -> raise Impossible
- | (annobj, Some ids_to_targets) ->
- (* If uri is the uri of an annotation, let's use the annotation file *)
- if is_annotation_uri uri then
-(* CSC: la roba annotata non dovrebbe piu' servire
- AnnotationParser.annotate (Getter.get_ann uri) ids_to_targets ;
-*) assert false ;
- try
- (annobj, ids_to_targets, HashTable.find hashtable (uri,0))
- with
- Not_found ->
- let obj = Deannotate.deannotate_obj annobj in
- let output = Unchecked obj in
- HashTable.add hashtable (uri,0) output ;
- (annobj, ids_to_targets, output)
-;;
-
-
(* get_obj uri *)
(* returns the cic object whose uri is uri. If the term is not just in cache, *)
(* then it is parsed via CicParser.term_of_xml from the file whose name is *)
| Cooked obj -> obj
;;
-(* get_annobj uri *)
-(* returns the cic object whose uri is uri either in annotated and *)
-(* deannotated form. The term is put into the cache if it's not there yet. *)
-let get_annobj uri =
- let (ann, ids_to_targets, deann) = get_annobj_and_type_checking_info uri in
- let deannobj =
- match deann with
- Unchecked obj -> obj
- | Frozen _ -> raise (CircularDependency (UriManager.string_of_uri uri))
- | Cooked obj -> obj
- in
- (ann, ids_to_targets, deannobj)
-;;
-
(*CSC Commento falso *)
(* get_obj uri *)
(* returns the cooked cic object whose uri is uri. The term must be present *)