X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=64ee58427b4bfb8c571b9e62f630e6425117010b;hb=6912a028bef118d8e9d7c2847200510a9b055c6a;hp=bf75243ec4300773479f1fe6b2c4dbbb356fee9e;hpb=5a92117eeff70048d29e91ba24e113155d956e1b;p=helm.git

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index bf75243ec..64ee58427 100644
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -36,60 +36,62 @@
 (*                                                                            *)
 (******************************************************************************)
 
-exception Warnings;;
+exception Getter_failure of string * string
+exception Parser_failure of string
 
-class warner =
-  object 
-    method warn w =
-      print_endline ("WARNING: " ^ w) ;
-      (raise Warnings : unit)
-  end
-;;
-
-exception EmptyUri;;
+  (** 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
 
-(* 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
-   | 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
-;;
+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. process_annotations is true if the annotations do really  *)
-(* matter                                                                    *)
-let term_of_xml filename uri process_annotations =
- let module Y = Pxp_yacc in
-  try 
-    let d =
-      (* sets the current base uri to resolve relative URIs *)
-      CicParser3.current_sp := tokens_of_uri uri ;
-      CicParser3.current_uri := uri ;
-      CicParser3.process_annotations := process_annotations ;
-      CicParser3.ids_to_targets :=
-       if process_annotations then Some (Hashtbl.create 500) else None ;
-      let config = {Y.default_config with Y.warner = new warner} in
-      Y.parse_document_entity config
-(*PXP       (Y.ExtID (Pxp_types.System filename,
-         new Pxp_reader.resolve_as_file ~url_of_id ()))
-*)     (PxpUriResolver.from_file filename)
-       CicParser3.domspec
-    in
-     let ids_to_targets = !CicParser3.ids_to_targets in
-      let res = (CicParser2.get_term d#root, ids_to_targets) in
-       CicParser3.ids_to_targets := None ; (* let's help the GC *)
-       res
-  with
-   e ->
-     print_endline ("Filename: " ^ filename ^ "\nException: ") ;
-     print_endline (Pxp_types.string_of_exn e) ;
-     raise e
-;;
+(* representation.                                                           *)
+let annobj_of_xml filename filenamebody =
+  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)
+