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