]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic/cicParser.ml
- added handling of exceptions embedded in xml documents (usually coming
[helm.git] / helm / ocaml / cic / cicParser.ml
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)