1 (* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
26 (******************************************************************************)
30 (* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
33 (* This is the main (top level) module of a parser for cic objects from xml *)
34 (* files to the internal representation. It uses the modules cicParser2 *)
35 (* (objects level) and cicParser3 (terms level) *)
37 (******************************************************************************)
42 exception Getter_failure of string * string
43 exception Parser_failure of string
45 (** tries to recover from a parse error caused by the parsing of a getter
46 * error message (e.g. Key_not_found exception). Unfortunately we have to
47 * re-parse xml document to extract exception data *)
48 let try_recover exn filename =
52 Pxp_ev_parser.create_entity_manager ~is_document:true
53 PxpHelmConf.pxp_config (Pxp_types.from_file filename)
56 Pxp_ev_parser.create_pull_parser PxpHelmConf.pxp_config
57 (`Entry_document []) entity_manager
62 | Some (Pxp_types.E_start_tag ("html", attrs, _, _)) ->
63 let exn = List.assoc "helm:exception" attrs in
65 try List.assoc "helm:exception_arg" attrs with Not_found -> ""
67 rc := Some (Getter_failure (exn, arg))
71 with _ -> raise (Parser_failure (Printexc.to_string exn)));
73 | None -> raise (Parser_failure (Printexc.to_string exn))
74 | Some exn -> raise exn
76 let parse_document filename =
78 Pxp_tree_parser.parse_document_entity PxpHelmConf.pxp_config
79 (Pxp_types.from_file ~alt:[PxpUrlResolver.url_resolver] filename)
82 raise (try_recover exn filename)
84 (* given the filename of an xml file of a cic object it returns its internal *)
86 let annobj_of_xml uri filename filenamebody =
87 CicParser3.set_uri uri;
89 let doc = parse_document filename in
90 let docroot = doc#root in
91 match filenamebody with
94 let docbody = parse_document filename in
95 docroot,Some docbody#root
97 CicParser2.get_term root rootbody
99 let obj_of_xml uri filename filenamebody =
100 Deannotate.deannotate_obj (annobj_of_xml uri filename filenamebody)