]> matita.cs.unibo.it Git - helm.git/blob - components/xmldiff/xmlDiff.ml
fixed generation of letins
[helm.git] / components / xmldiff / xmlDiff.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 (* $Id$ *)
27
28 let mathmlns = "http://www.w3.org/1998/Math/MathML";;
29 let xmldiffns = "http://helm.cs.unibo.it/XmlDiff";;
30 let helmns = "http://www.cs.unibo.it/helm";;
31
32 let ds_selection      = Gdome.domString "selection";;
33 let ds_2              = Gdome.domString "2";;
34 let ds_mathmlns       = Gdome.domString mathmlns;;
35 let ds_m_style        = Gdome.domString "m:mstyle";;
36 let ds_mathbackground = Gdome.domString "mathbackground";;
37 let ds_xmldiffns      = Gdome.domString xmldiffns;;
38 let ds_xmldiff_type   = Gdome.domString "xmldiff:type";;
39 let ds_fake           = Gdome.domString "fake";;
40 let ds_helmns         = Gdome.domString helmns;;
41 let ds_xref           = Gdome.domString "xref";;
42 let ds_type           = Gdome.domString "type";;
43 let ds_yellow         = Gdome.domString "yellow";;
44 let ds_green          = Gdome.domString "#00ff00";;
45 let ds_maction        = Gdome.domString "maction";;
46 let ds_mtr            = Gdome.domString "mtr";;
47 let ds_mtd            = Gdome.domString "mtd";;
48
49 type highlighted_nodes = Gdome.node list;;
50
51 let rec make_visible (n: Gdome.node) =
52  match n#get_parentNode with
53     None -> ()
54   | Some p ->
55      match p#get_namespaceURI, p#get_localName with
56         Some nu, Some ln when
57          nu#equals ds_mathmlns && ln#equals ds_maction ->
58           (new Gdome.element_of_node p)#setAttribute
59             ~name:ds_selection
60              ~value:ds_2 ;
61           make_visible p
62       | _,_ -> make_visible p
63 ;;
64
65 let highlight_node_total_time = ref 0.0;;
66
67 let highlight_node ?(color=ds_yellow) (doc: Gdome.document) (n: Gdome.node) =
68  let highlight (n: Gdome.node) =
69   let highlighter =
70    doc#createElementNS
71     ~namespaceURI:(Some ds_mathmlns)
72     ~qualifiedName:ds_m_style
73   in
74    highlighter#setAttribute ~name:ds_mathbackground ~value:color ;
75    highlighter#setAttributeNS
76     ~namespaceURI:(Some ds_xmldiffns)
77     ~qualifiedName:ds_xmldiff_type
78     ~value:ds_fake ;
79    let parent = 
80     match n#get_parentNode with
81        None -> assert false
82      | Some p -> p
83    in
84     ignore
85      (parent#replaceChild ~oldChild:n ~newChild:(highlighter :> Gdome.node)) ;
86     ignore (highlighter#appendChild n) ;
87     (highlighter :> Gdome.node)
88  in
89   let rec find_mstylable_node n =
90    match n#get_namespaceURI, n#get_localName with
91       Some nu, Some ln when
92        nu#equals ds_mathmlns &&
93         (not (ln#equals ds_mtr)) && (not (ln#equals ds_mtd)) -> n
94     | Some nu, Some ln when
95        nu#equals ds_mathmlns &&
96         ln#equals ds_mtr || ln#equals ds_mtd ->
97          let true_child =
98           match n#get_firstChild with
99              None -> assert false
100            | Some n -> n
101          in
102           find_mstylable_node true_child
103     | _,_ ->
104       match n#get_parentNode with
105          None -> assert false
106        | Some p -> find_mstylable_node p
107   in
108    let highlighter = highlight (find_mstylable_node n) in
109     make_visible highlighter ;
110     highlighter
111 ;;
112
113 let iter_children ~f (n:Gdome.node) =
114  let rec aux =
115   function
116      None -> ()
117    | Some n ->
118       let sibling = n#get_nextSibling in
119        (f n) ;
120        aux sibling
121  in
122   aux n#get_firstChild
123 ;;
124
125 let highlight_nodes ~xrefs (doc:Gdome.document) =
126  let highlighted = ref [] in
127  let rec aux (n:Gdome.element) =
128   let attributeNS =
129     (n#getAttributeNS ~namespaceURI:ds_helmns
130      ~localName:ds_xref)#to_string in
131   if List.mem attributeNS xrefs then
132    highlighted :=
133     (highlight_node ~color:ds_green doc (n :> Gdome.node))::
134     !highlighted ;
135    iter_children (n :> Gdome.node)
136     ~f:(function n ->
137          if n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE then
138           aux (new Gdome.element_of_node n))
139  in
140   aux doc#get_documentElement ;
141   !highlighted
142 ;;
143
144 let dim_nodes =
145  List.iter 
146   (function (n : Gdome.node) ->
147     assert
148      (n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE &&
149       ((new Gdome.element_of_node n)#getAttributeNS
150         ~namespaceURI:ds_xmldiffns
151         ~localName:ds_type)#equals ds_fake) ;
152     let true_child =
153      match n#get_firstChild with
154         None -> assert false
155       | Some n -> n in
156     let p =
157      match n#get_parentNode with
158         None -> assert false
159       | Some n -> n
160     in
161      ignore (p#replaceChild ~oldChild:n ~newChild:true_child)
162   )
163 ;;
164
165 let update_dom ~(from : Gdome.document) (d : Gdome.document) =
166  let rec aux (p: Gdome.node) (f: Gdome.node) (t: Gdome.node) =
167  let replace t1 =
168   if
169    t1 = GdomeNodeTypeT.ELEMENT_NODE &&
170    ((new Gdome.element_of_node f)#getAttributeNS
171      ~namespaceURI:ds_xmldiffns
172      ~localName:ds_type)#equals ds_fake
173   then
174    let true_child =
175     match f#get_firstChild with
176        None -> assert false
177      | Some n -> n
178    in
179     begin
180      ignore (p#replaceChild ~oldChild:f ~newChild:true_child) ;
181      aux p true_child t
182     end
183   else
184    let t' = from#importNode t true in
185     ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
186     (* ignore (highlight_node from t') *)
187   in
188   match
189    f#get_nodeType,t#get_nodeType
190   with
191      GdomeNodeTypeT.TEXT_NODE,GdomeNodeTypeT.TEXT_NODE ->
192       (match f#get_nodeValue, t#get_nodeValue with
193           Some v, Some v' when v#equals v' -> ()
194         | Some _, (Some _ as v') -> f#set_nodeValue v'
195         | _,_ -> assert false)
196    | GdomeNodeTypeT.ELEMENT_NODE as t1,GdomeNodeTypeT.ELEMENT_NODE ->
197       (match
198         f#get_namespaceURI,t#get_namespaceURI,f#get_localName,t#get_localName
199        with
200         Some nu, Some nu', Some ln, Some ln' when
201          ln#equals ln' && nu#equals nu' ->
202           begin
203            match f#get_attributes, t#get_attributes with
204               Some fattrs, Some tattrs ->
205                let flen = fattrs#get_length in
206                let tlen = tattrs#get_length in
207                 let processed = ref [] in
208                 for i = 0 to flen -1 do
209                  match fattrs#item i with
210                     None -> () (* CSC: sigh, togliere un nodo rompe fa decrescere la lunghezza ==> passare a un while *)
211                   | Some attr ->
212                       match attr#get_namespaceURI with
213                          None ->
214                           (* Back to DOM Level 1 ;-( *)
215                           begin
216                            let name = attr#get_nodeName in
217                             match tattrs#getNamedItem ~name with
218                                None ->
219                                ignore (fattrs#removeNamedItem ~name)
220                              | Some attr' ->
221                                 processed :=
222                                  (None,Some name)::!processed ;
223                                 match attr#get_nodeValue, attr'#get_nodeValue with
224                                    Some v1, Some v2 when
225                                        v1#equals v2
226                                     || (name#equals ds_selection &&
227                                         nu#equals ds_mathmlns &&
228                                         ln#equals ds_maction)
229                                     ->
230                                      ()
231                                  | Some v1, Some v2 ->
232                                     let attr'' = from#importNode attr' true in
233                                      ignore (fattrs#setNamedItem attr'')
234                                  | _,_ -> assert false
235                           end
236                        | Some namespaceURI ->
237                           let localName = 
238                            match attr#get_localName with
239                              Some v -> v
240                             | None -> assert false
241                           in
242                            match
243                             tattrs#getNamedItemNS ~namespaceURI ~localName
244                            with
245                               None ->
246                                ignore
247                                 (fattrs#removeNamedItemNS
248                                   ~namespaceURI ~localName)
249                             | Some attr' ->
250                                processed :=
251                                 (Some namespaceURI,Some localName)::!processed ;
252                                 match attr#get_nodeValue, attr'#get_nodeValue with
253                                    Some v1, Some v2 when
254                                     v1#equals v2 ->
255                                      ()
256                                  | Some _, Some _ ->
257                                     let attr'' = from#importNode attr' true in
258                                      ignore (fattrs#setNamedItem attr'')
259                                  | _,_ -> assert false
260                 done ;
261                 for i = 0 to tlen -1 do
262                  match tattrs#item i with
263                     None -> assert false
264                   | Some attr ->
265                      let namespaceURI,localName =
266                       match attr#get_namespaceURI with
267                          None ->
268                           None,attr#get_nodeName
269                        | Some namespaceURI as v ->
270                          v, match attr#get_localName with
271                             None -> assert false
272                           | Some v -> v
273                      in
274                       if
275                        not
276                         (List.exists
277                           (function
278                               None,Some localName' ->
279                                (match namespaceURI with
280                                    None ->
281                                     localName#equals localName'
282                                  | Some _ -> false)
283                             | Some namespaceURI', Some localName' ->
284                                (match namespaceURI with
285                                    None -> false
286                                  | Some namespaceURI ->
287                                     localName#equals localName' &&
288                                     namespaceURI#equals namespaceURI'
289                                )
290                             | _,_ -> assert false
291                           ) !processed)
292                       then
293                        let attr' = from#importNode attr false in
294                         ignore (fattrs#setNamedItem attr')
295                 done
296             | _,_ -> assert false
297           end ;
298           let rec dumb_diff =
299            function
300               [],[] -> ()
301             | he1::tl1,he2::tl2 ->
302                aux f he1 he2 ;
303                dumb_diff (tl1,tl2)
304             | [],tl2 ->
305                List.iter
306                 (function n ->
307                   let n' = from#importNode n true in
308                     ignore (f#appendChild n') ;
309                     (* ignore (highlight_node from n') *)
310                     ()
311                 ) tl2
312             | tl1,[] ->
313                List.iter (function n -> ignore (f#removeChild n)) tl1
314           in
315            let node_list_of_nodeList n =
316             let rec aux =
317              function
318                 None -> []
319               | Some n when
320                     n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE
321                  or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE ->
322                   n::(aux n#get_nextSibling)
323               | Some n ->
324                 aux n#get_nextSibling
325             in
326              aux n#get_firstChild
327            in
328             dumb_diff
329              (node_list_of_nodeList f, node_list_of_nodeList t)
330       | _,_,_,_ -> replace t1
331       )
332    | t1,t2 when
333       (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) &&
334       (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) ->
335        replace t1
336    | _,_ -> assert false
337  in
338   try
339    aux (d :> Gdome.node)
340     (from#get_documentElement :> Gdome.node)
341     (d#get_documentElement :> Gdome.node)
342   with
343      (GdomeInit.DOMException (e,msg) as ex) -> raise ex
344   | e -> raise e
345 ;;