]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/cic_transformations/xml2Gdome.ml
Added Coer/Coercions print_kind
[helm.git] / helm / ocaml / cic_transformations / xml2Gdome.ml
1 (* Copyright (C) 2000-2002, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  *)
25
26 let document_of_xml (domImplementation : Gdome.domImplementation) strm =
27  let module G = Gdome in
28  let module X = Xml in
29   let rec update_namespaces ((defaultns,bindings) as namespaces) =
30    function
31       [] -> namespaces
32     | (None,"xmlns",value)::tl ->
33        update_namespaces (Some (Gdome.domString value),bindings) tl
34     | (prefix,name,value)::tl when prefix = Some "xmlns"  ->
35         update_namespaces (defaultns,(name,Gdome.domString value)::bindings) tl
36     | _::tl -> update_namespaces namespaces tl in
37   let rec namespace_of_prefix (defaultns,bindings) =
38    function
39       None -> None
40     | Some "xmlns" -> Some (Gdome.domString "xml-ns")
41     | Some p' ->
42        try
43         Some (List.assoc p' bindings)
44        with
45         Not_found ->
46          raise
47           (Failure ("The prefix " ^ p' ^ " is not bound to any namespace")) in
48   let get_qualified_name p n =
49    match p with
50       None -> Gdome.domString n
51     | Some p' -> Gdome.domString (p' ^ ":" ^ n) in
52   let root_prefix,root_name,root_attributes,root_content =
53    ignore (Stream.next strm) ; (* to skip the <?xml ...?> declaration *)
54    ignore (Stream.next strm) ; (* to skip the DOCTYPE declaration *)
55    match Stream.next strm with
56       X.Empty(p,n,l) -> p,n,l,[<>]
57     | X.NEmpty(p,n,l,c) -> p,n,l,c
58     | _ -> assert false
59   in
60    let namespaces = update_namespaces (None,[]) root_attributes in
61    let namespaceURI = namespace_of_prefix namespaces root_prefix in
62    let document =
63     domImplementation#createDocument ~namespaceURI
64      ~qualifiedName:(get_qualified_name root_prefix root_name)
65      ~doctype:None
66    in
67    let rec aux namespaces (node : Gdome.node) =
68     parser
69       [< 'X.Str a ; s >] ->
70         let textnode = document#createTextNode ~data:(Gdome.domString a) in
71          ignore (node#appendChild ~newChild:(textnode :> Gdome.node)) ;
72          aux namespaces node s
73     | [< 'X.Empty(p,n,l) ; s >] ->
74         let namespaces' = update_namespaces namespaces l in
75          let namespaceURI = namespace_of_prefix namespaces' p in
76           let element =
77            document#createElementNS ~namespaceURI
78             ~qualifiedName:(get_qualified_name p n)
79           in
80            List.iter
81             (function (p,n,v) ->
82               if p = None then
83                element#setAttribute ~name:(Gdome.domString n)
84                 ~value:(Gdome.domString v)
85               else
86                let namespaceURI = namespace_of_prefix namespaces' p in
87                 element#setAttributeNS
88                  ~namespaceURI
89                  ~qualifiedName:(get_qualified_name p n)
90                  ~value:(Gdome.domString v)
91             ) l ;
92           ignore
93            (node#appendChild
94              ~newChild:(element : Gdome.element :> Gdome.node)) ;
95           aux namespaces node s
96     | [< 'X.NEmpty(p,n,l,c) ; s >] ->
97         let namespaces' = update_namespaces namespaces l in
98          let namespaceURI = namespace_of_prefix namespaces' p in
99           let element =
100            document#createElementNS ~namespaceURI
101             ~qualifiedName:(get_qualified_name p n)
102           in
103            List.iter
104             (function (p,n,v) ->
105               if p = None then
106                element#setAttribute ~name:(Gdome.domString n)
107                 ~value:(Gdome.domString v)
108               else
109                let namespaceURI = namespace_of_prefix namespaces' p in
110                 element#setAttributeNS ~namespaceURI
111                  ~qualifiedName:(get_qualified_name p n)
112                  ~value:(Gdome.domString v)
113             ) l ;
114            ignore (node#appendChild ~newChild:(element :> Gdome.node)) ;
115            aux namespaces' (element :> Gdome.node) c ;
116            aux namespaces node s
117     | [< >] -> ()
118    in
119     let root = document#get_documentElement in
120      List.iter
121       (function (p,n,v) ->
122         if p = None then
123          root#setAttribute ~name:(Gdome.domString n)
124           ~value:(Gdome.domString v)
125         else
126          let namespaceURI = namespace_of_prefix namespaces p in
127           root#setAttributeNS ~namespaceURI
128            ~qualifiedName:(get_qualified_name p n)
129            ~value:(Gdome.domString v)
130       ) root_attributes ;
131      aux namespaces (root : Gdome.element :> Gdome.node) root_content ;
132      document
133 ;;