X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser.ml;h=c46a20a982d68c260f61eb6ce4e55ae81462db15;hb=d47a2eaf9d30d56cbc230d8bf8c37054ebeae54f;hp=64ee58427b4bfb8c571b9e62f630e6425117010b;hpb=9c313992f130290e8b8d97a7b199b9171784cecf;p=helm.git

diff --git a/helm/ocaml/cic/cicParser.ml b/helm/ocaml/cic/cicParser.ml
index 64ee58427..c46a20a98 100644
--- a/helm/ocaml/cic/cicParser.ml
+++ b/helm/ocaml/cic/cicParser.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2000-2005, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -23,75 +23,5 @@
  * http://cs.unibo.it/helm/.
  *)
 
-(******************************************************************************)
-(*                                                                            *)
-(*                               PROJECT HELM                                 *)
-(*                                                                            *)
-(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
-(*                                 24/01/2000                                 *)
-(*                                                                            *)
-(* This is the main (top level) module of a parser for cic objects from xml   *)
-(* files to the internal representation. It uses the modules cicParser2       *)
-(* (objects level) and cicParser3 (terms level)                               *)
-(*                                                                            *)
-(******************************************************************************)
-
-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 =
-  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)
+include CicPushParser.CicParser