X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=f0d3e800fe11f84a44944119866c8374c393e142;hb=09aa799947c84148221af82e94e911adea8fd1e6;hp=bf75243ec4300773479f1fe6b2c4dbbb356fee9e;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index bf75243ec..f0d3e800f 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -64,18 +64,14 @@ let tokens_of_uri uri = ;; (* given the filename of an xml file of a cic object it returns its internal *) -(* representation. process_annotations is true if the annotations do really *) -(* matter *) -let term_of_xml filename uri process_annotations = +(* representation. *) +let annobj_of_xml filename uri = let module Y = Pxp_yacc in try let d = (* sets the current base uri to resolve relative URIs *) CicParser3.current_sp := tokens_of_uri uri ; CicParser3.current_uri := uri ; - CicParser3.process_annotations := process_annotations ; - CicParser3.ids_to_targets := - if process_annotations then Some (Hashtbl.create 500) else None ; let config = {Y.default_config with Y.warner = new warner} in Y.parse_document_entity config (*PXP (Y.ExtID (Pxp_types.System filename, @@ -83,13 +79,14 @@ let term_of_xml filename uri process_annotations = *) (PxpUriResolver.from_file filename) CicParser3.domspec in - let ids_to_targets = !CicParser3.ids_to_targets in - let res = (CicParser2.get_term d#root, ids_to_targets) in - CicParser3.ids_to_targets := None ; (* let's help the GC *) - res + CicParser2.get_term d#root with e -> print_endline ("Filename: " ^ filename ^ "\nException: ") ; print_endline (Pxp_types.string_of_exn e) ; raise e ;; + +let obj_of_xml filename uri = + Deannotate.deannotate_obj (annobj_of_xml filename uri) +;;