From: Stefano Zacchiroli <zack@upsilon.cc>
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  *)