1 (* Copyright (C) 2000-2002, 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/.
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";;
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";;
49 type highlighted_nodes = Gdome.node list;;
51 let rec make_visible (n: Gdome.node) =
52 match n#get_parentNode with
55 match p#get_namespaceURI, p#get_localName with
57 nu#equals ds_mathmlns && ln#equals ds_maction ->
58 (new Gdome.element_of_node p)#setAttribute
62 | _,_ -> make_visible p
65 let highlight_node_total_time = ref 0.0;;
67 let highlight_node ?(color=ds_yellow) (doc: Gdome.document) (n: Gdome.node) =
68 let highlight (n: Gdome.node) =
71 ~namespaceURI:(Some ds_mathmlns)
72 ~qualifiedName:ds_m_style
74 highlighter#setAttribute ~name:ds_mathbackground ~value:color ;
75 highlighter#setAttributeNS
76 ~namespaceURI:(Some ds_xmldiffns)
77 ~qualifiedName:ds_xmldiff_type
80 match n#get_parentNode with
85 (parent#replaceChild ~oldChild:n ~newChild:(highlighter :> Gdome.node)) ;
86 ignore (highlighter#appendChild n) ;
87 (highlighter :> Gdome.node)
89 let rec find_mstylable_node n =
90 match n#get_namespaceURI, n#get_localName with
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 ->
98 match n#get_firstChild with
102 find_mstylable_node true_child
104 match n#get_parentNode with
106 | Some p -> find_mstylable_node p
108 let highlighter = highlight (find_mstylable_node n) in
109 make_visible highlighter ;
113 let iter_children ~f (n:Gdome.node) =
118 let sibling = n#get_nextSibling in
125 let highlight_nodes ~xrefs (doc:Gdome.document) =
126 let highlighted = ref [] in
127 let rec aux (n:Gdome.element) =
129 (n#getAttributeNS ~namespaceURI:ds_helmns
130 ~localName:ds_xref)#to_string in
131 if List.mem attributeNS xrefs then
133 (highlight_node ~color:ds_green doc (n :> Gdome.node))::
135 iter_children (n :> Gdome.node)
137 if n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE then
138 aux (new Gdome.element_of_node n))
140 aux doc#get_documentElement ;
146 (function (n : Gdome.node) ->
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) ;
153 match n#get_firstChild with
157 match n#get_parentNode with
161 ignore (p#replaceChild ~oldChild:n ~newChild:true_child)
165 let update_dom ~(from : Gdome.document) (d : Gdome.document) =
166 let rec aux (p: Gdome.node) (f: Gdome.node) (t: Gdome.node) =
169 t1 = GdomeNodeTypeT.ELEMENT_NODE &&
170 ((new Gdome.element_of_node f)#getAttributeNS
171 ~namespaceURI:ds_xmldiffns
172 ~localName:ds_type)#equals ds_fake
175 match f#get_firstChild with
180 ignore (p#replaceChild ~oldChild:f ~newChild:true_child) ;
184 let t' = from#importNode t true in
185 ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
186 (* ignore (highlight_node from t') *)
189 f#get_nodeType,t#get_nodeType
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 ->
198 f#get_namespaceURI,t#get_namespaceURI,f#get_localName,t#get_localName
200 Some nu, Some nu', Some ln, Some ln' when
201 ln#equals ln' && nu#equals nu' ->
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 *)
212 match attr#get_namespaceURI with
214 (* Back to DOM Level 1 ;-( *)
216 let name = attr#get_nodeName in
217 match tattrs#getNamedItem ~name with
219 ignore (fattrs#removeNamedItem ~name)
222 (None,Some name)::!processed ;
223 match attr#get_nodeValue, attr'#get_nodeValue with
224 Some v1, Some v2 when
226 || (name#equals ds_selection &&
227 nu#equals ds_mathmlns &&
228 ln#equals ds_maction)
231 | Some v1, Some v2 ->
232 let attr'' = from#importNode attr' true in
233 ignore (fattrs#setNamedItem attr'')
234 | _,_ -> assert false
236 | Some namespaceURI ->
238 match attr#get_localName with
240 | None -> assert false
243 tattrs#getNamedItemNS ~namespaceURI ~localName
247 (fattrs#removeNamedItemNS
248 ~namespaceURI ~localName)
251 (Some namespaceURI,Some localName)::!processed ;
252 match attr#get_nodeValue, attr'#get_nodeValue with
253 Some v1, Some v2 when
257 let attr'' = from#importNode attr' true in
258 ignore (fattrs#setNamedItem attr'')
259 | _,_ -> assert false
261 for i = 0 to tlen -1 do
262 match tattrs#item i with
265 let namespaceURI,localName =
266 match attr#get_namespaceURI with
268 None,attr#get_nodeName
269 | Some namespaceURI as v ->
270 v, match attr#get_localName with
278 None,Some localName' ->
279 (match namespaceURI with
281 localName#equals localName'
283 | Some namespaceURI', Some localName' ->
284 (match namespaceURI with
286 | Some namespaceURI ->
287 localName#equals localName' &&
288 namespaceURI#equals namespaceURI'
290 | _,_ -> assert false
293 let attr' = from#importNode attr false in
294 ignore (fattrs#setNamedItem attr')
296 | _,_ -> assert false
301 | he1::tl1,he2::tl2 ->
307 let n' = from#importNode n true in
308 ignore (f#appendChild n') ;
309 (* ignore (highlight_node from n') *)
313 List.iter (function n -> ignore (f#removeChild n)) tl1
315 let node_list_of_nodeList n =
320 n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE
321 or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE ->
322 n::(aux n#get_nextSibling)
324 aux n#get_nextSibling
329 (node_list_of_nodeList f, node_list_of_nodeList t)
330 | _,_,_,_ -> replace t1
333 (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) &&
334 (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) ->
336 | _,_ -> assert false
339 aux (d :> Gdome.node)
340 (from#get_documentElement :> Gdome.node)
341 (d#get_documentElement :> Gdome.node)
343 (GdomeInit.DOMException (e,msg) as ex) -> raise ex