From: Stefano Zacchiroli Date: Mon, 24 Jan 2005 16:15:11 +0000 (+0000) Subject: - added handling of exceptions embedded in xml documents (usually coming X-Git-Tag: V_0_1_0~96 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=9c313992f130290e8b8d97a7b199b9171784cecf;p=helm.git - added handling of exceptions embedded in xml documents (usually coming from http_getter) - added exception Getter_failure which wraps the above exception - added exception Parser_failure for generic errors - removed useless EmptyUri exception --- diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml index 5ad48b079..64ee58427 100644 --- a/helm/ocaml/cic/cicParser.ml +++ b/helm/ocaml/cic/cicParser.ml @@ -36,36 +36,61 @@ (* *) (******************************************************************************) -exception EmptyUri of string +exception Getter_failure of string * string +exception Parser_failure of string + + (** tries to recover from a parse error caused by the parsing of a getter + * error message (e.g. Key_not_found exception). Unfortunately we have to + * re-parse xml document to extract exception data *) +let try_recover exn filename = + let rc = ref None in + (try + let entity_manager = + Pxp_ev_parser.create_entity_manager ~is_document:true + PxpHelmConf.pxp_config (Pxp_types.from_file filename) + in + let pull_parser = + Pxp_ev_parser.create_pull_parser PxpHelmConf.pxp_config + (`Entry_document []) entity_manager + in + let rec find_exn p = + match p () with + | None -> () + | Some (Pxp_types.E_start_tag ("html", attrs, _, _)) -> + let exn = List.assoc "helm:exception" attrs in + let arg = + try List.assoc "helm:exception_arg" attrs with Not_found -> "" + in + rc := Some (Getter_failure (exn, arg)) + | _ -> find_exn p + in + find_exn pull_parser + with _ -> raise (Parser_failure (Printexc.to_string exn))); + match !rc with + | None -> raise (Parser_failure (Printexc.to_string exn)) + | Some exn -> raise exn + +let parse_document filename = + try + Pxp_tree_parser.parse_document_entity PxpHelmConf.pxp_config + (Pxp_types.from_file ~alt:[PxpUrlResolver.url_resolver] filename) + CicParser3.domspec + with exn -> + raise (try_recover exn filename) (* given the filename of an xml file of a cic object it returns its internal *) (* representation. *) let annobj_of_xml filename filenamebody = - try - let root, rootbody = - let config = PxpHelmConf.pxp_config in - let doc = - Pxp_tree_parser.parse_document_entity config - (Pxp_types.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 = - Pxp_tree_parser.parse_document_entity config - (Pxp_types.from_file ~alt:[PxpUrlResolver.url_resolver] filename) - CicParser3.domspec - in - docroot,Some docbody#root - in - CicParser2.get_term root rootbody - with - e -> - prerr_endline ("Filenames: " ^ filename ^ - (match filenamebody with None -> "" | Some s -> ", " ^ s)) ; - prerr_endline ("Exception: " ^ Pxp_types.string_of_exn e) ; - raise e + let root, rootbody = + let doc = parse_document filename in + let docroot = doc#root in + match filenamebody with + None -> docroot,None + | Some filename -> + let docbody = parse_document filename in + docroot,Some docbody#root + in + CicParser2.get_term root rootbody 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 a965cf262..048df36a3 100644 --- a/helm/ocaml/cic/cicParser.mli +++ b/helm/ocaml/cic/cicParser.mli @@ -36,6 +36,14 @@ (* *) (******************************************************************************) + (** raised for exception received by the getter (i.e. embedded in the source + * XML document). Arguments are values of "helm:exception" and + * "helm:exception_arg" attributes *) +exception Getter_failure of string * string + + (** generic parser failure *) +exception Parser_failure of string + (* 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 *)