From: Claudio Sacerdoti Coen Date: Mon, 28 Oct 2002 10:47:14 +0000 (+0000) Subject: - for/of attribute no more checked ;-( X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=96cfa10549351789f8eb97cbcefe01c68738b5ec;p=helm.git - for/of attribute no more checked ;-( - parsing does not require any more the current uri (that was unclear for CurrentProof) - as a consequence of the previous change the parser should now be reentrant --- diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 5149cfd6a..cb3a064fd 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -48,50 +48,31 @@ class warner = exception EmptyUri of string;; -(* given an uri u it returns the list of tokens of the base uri of u *) -(* e.g.: token_of_uri "cic:/a/b/c/d.xml" returns ["a" ; "b" ; "c"] *) -let tokens_of_uri uri = - let uri' = UriManager.string_of_uri uri in - let rec chop_list = - function - [] -> raise (EmptyUri uri') - | [fn] -> [] - | he::[fn] -> [he] - | he::tl -> he::(chop_list tl) - in - let trimmed_uri = Str.replace_first (Str.regexp "cic:") "" uri' in - let list_of_tokens = Str.split (Str.regexp "/") trimmed_uri in - chop_list list_of_tokens -;; - (* given the filename of an xml file of a cic object it returns its internal *) (* representation. *) -let annobj_of_xml filename filenamebody uri = +let annobj_of_xml filename filenamebody = let module Y = Pxp_yacc in try let root, rootbody = - (* sets the current base uri to resolve relative URIs *) - CicParser3.current_sp := tokens_of_uri uri ; - CicParser3.current_uri := uri ; - let config = {Y.default_config with Y.warner = new warner} in - let doc = - Y.parse_document_entity config - (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) - CicParser3.domspec in + let config = {Y.default_config with Y.warner = new warner} in + let doc = + Y.parse_document_entity config + (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) + CicParser3.domspec in (* CSC: Until PXP bug is resolved *) PxpUrlResolver.url_resolver#close_all ; - let docroot = doc#root in - match filenamebody with - None -> docroot,None - | Some filename -> - let docbody = - Y.parse_document_entity config - (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) - CicParser3.domspec - in + let docroot = doc#root in + match filenamebody with + None -> docroot,None + | Some filename -> + let docbody = + Y.parse_document_entity config + (Y.from_file ~alt:[PxpUrlResolver.url_resolver] filename) + CicParser3.domspec + in (* CSC: Until PXP bug is resolved *) PxpUrlResolver.url_resolver#close_all ; - docroot,Some docbody#root + docroot,Some docbody#root in CicParser2.get_term root rootbody with @@ -102,6 +83,6 @@ PxpUrlResolver.url_resolver#close_all ; raise e ;; -let obj_of_xml filename filenamebody uri = - Deannotate.deannotate_obj (annobj_of_xml filename filenamebody uri) +let obj_of_xml filename filenamebody = + Deannotate.deannotate_obj (annobj_of_xml filename filenamebody) ;; diff --git a/helm/ocaml/cic/cicParser.mli b/helm/ocaml/cic/cicParser.mli index 0d0a8172b..a965cf262 100644 --- a/helm/ocaml/cic/cicParser.mli +++ b/helm/ocaml/cic/cicParser.mli @@ -36,14 +36,14 @@ (* *) (******************************************************************************) -(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* given the filename of an xml file of a cic object, it returns *) (* its internal annotated representation. In the case of constants (whose *) (* type is splitted from the body), a second xml file (for the body) must be *) (* provided. *) -val annobj_of_xml : string -> string option -> UriManager.uri -> Cic.annobj +val annobj_of_xml : string -> string option -> Cic.annobj -(* given the filename of an xml file of a cic object and it's uri, it returns *) +(* given the filename of an xml file of a cic object, it returns *) (* its internal logical representation. In the case of constants (whose *) (* type is splitted from the body), a second xml file (for the body) must be *) (* provided. *) -val obj_of_xml : string -> string option -> UriManager.uri -> Cic.obj +val obj_of_xml : string -> string option -> Cic.obj diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index e74cf73d3..426ecf21a 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -194,26 +194,24 @@ let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody let nbodytype = nbody'#node_type in match nbodytype with D.T_element "ConstantBody" -> +(*CSC: the attribute "for" is ignored and not checked let for_ = string_of_attr (nbody'#attribute "for") in +*) let paramsbody = uri_list_of_attr (nbody'#attribute "params") in let xidbody = string_of_attr (nbody'#attribute "id") in let value = (get_content nbody')#extension#to_cic_term [] in - if paramsbody = params && - U.eq (U.uri_of_string for_) !CicParser3.current_uri - then + if paramsbody = params then C.AConstant (xid, Some xidbody, name, Some value, typ, params) else raise (IllFormedXml 6) | D.T_element "CurrentProof" -> +(*CSC: the attribute "of" is ignored and not checked let for_ = string_of_attr (nbody'#attribute "of") in +*) let xidbody = string_of_attr (nbody'#attribute "id") in - let value = (get_content nbody')#extension#to_cic_term [] in let sons = nbody'#sub_nodes in let (conjs, value) = get_conjs_value sons in - if U.eq (U.uri_of_string for_) !CicParser3.current_uri then - C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params) - else - raise (IllFormedXml 6) + C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params) | D.T_element _ | D.T_data | _ -> raise (IllFormedXml 6) diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml index 04bbb9029..02d22b321 100644 --- a/helm/ocaml/cic/cicParser3.ml +++ b/helm/ocaml/cic/cicParser3.ml @@ -41,13 +41,6 @@ exception IllFormedXml of int;; -(* The list of tokens of the current section path. *) -(* Used to resolve relative URIs *) -let current_sp = ref [];; - -(* The uri of the object been parsed *) -let current_uri = ref (UriManager.uri_of_string "cic:/.xml");; - (* Utility functions to map a markup attribute to something useful *) let cic_attr_of_xml_attr = diff --git a/helm/ocaml/cic/cicParser3.mli b/helm/ocaml/cic/cicParser3.mli index c3664c819..3c2f5d94c 100644 --- a/helm/ocaml/cic/cicParser3.mli +++ b/helm/ocaml/cic/cicParser3.mli @@ -41,9 +41,6 @@ exception IllFormedXml of int -val current_sp : string list ref -val current_uri : UriManager.uri ref - (* the "interface" of the class linked to each node of the dom tree *) class virtual cic_term : object ('a)