]> matita.cs.unibo.it Git - helm.git/commitdiff
- added handling of exceptions embedded in xml documents (usually coming
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 24 Jan 2005 16:15:11 +0000 (16:15 +0000)
  from http_getter)
- added exception Getter_failure which wraps the above exception
- added exception Parser_failure for generic errors
- removed useless EmptyUri exception

helm/ocaml/cic/cicParser.ml
helm/ocaml/cic/cicParser.mli

index 5ad48b0799d5906f458d5123f211781648f15104..64ee58427b4bfb8c571b9e62f630e6425117010b 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
-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)
index a965cf2626b06eff6127ad66e8a91b62fc30b149..048df36a360dbe3898f8be1b37bbe9b0070c2571 100644 (file)
 (*                                                                            *)
 (******************************************************************************)
 
+  (** 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  *)