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/.
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";;
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";;
47 type highlighted_nodes = Gdome.node list;;
49 let rec make_visible (n: Gdome.node) =
50 match n#get_parentNode with
53 match p#get_namespaceURI, p#get_localName with
55 nu#equals ds_mathmlns && ln#equals ds_maction ->
56 (new Gdome.element_of_node p)#setAttribute
60 | _,_ -> make_visible p
63 let highlight_node_total_time = ref 0.0;;
65 let highlight_node ?(color=ds_yellow) (doc: Gdome.document) (n: Gdome.node) =
66 let highlight (n: Gdome.node) =
69 ~namespaceURI:(Some ds_mathmlns)
70 ~qualifiedName:ds_m_style
72 highlighter#setAttribute ~name:ds_mathbackground ~value:color ;
73 highlighter#setAttributeNS
74 ~namespaceURI:(Some ds_xmldiffns)
75 ~qualifiedName:ds_xmldiff_type
78 match n#get_parentNode with
83 (parent#replaceChild ~oldChild:n ~newChild:(highlighter :> Gdome.node)) ;
84 ignore (highlighter#appendChild n) ;
85 (highlighter :> Gdome.node)
87 let rec find_mstylable_node n =
88 match n#get_namespaceURI, n#get_localName with
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 ->
96 match n#get_firstChild with
100 find_mstylable_node true_child
102 match n#get_parentNode with
104 | Some p -> find_mstylable_node p
106 let highlighter = highlight (find_mstylable_node n) in
107 make_visible highlighter ;
111 let iter_children ~f (n:Gdome.node) =
116 let sibling = n#get_nextSibling in
123 let highlight_nodes ~xrefs (doc:Gdome.document) =
124 let highlighted = ref [] in
125 let rec aux (n:Gdome.element) =
127 (n#getAttributeNS ~namespaceURI:ds_helmns
128 ~localName:ds_xref)#to_string in
129 if List.mem attributeNS xrefs then
131 (highlight_node ~color:ds_green doc (n :> Gdome.node))::
133 iter_children (n :> Gdome.node)
135 if n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE then
136 aux (new Gdome.element_of_node n))
138 aux doc#get_documentElement ;
144 (function (n : Gdome.node) ->
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) ;
151 match n#get_firstChild with
155 match n#get_parentNode with
159 ignore (p#replaceChild ~oldChild:n ~newChild:true_child)
163 let update_dom ~(from : Gdome.document) (d : Gdome.document) =
164 let rec aux (p: Gdome.node) (f: Gdome.node) (t: Gdome.node) =
167 t1 = GdomeNodeTypeT.ELEMENT_NODE &&
168 ((new Gdome.element_of_node f)#getAttributeNS
169 ~namespaceURI:ds_xmldiffns
170 ~localName:ds_type)#equals ds_fake
173 match f#get_firstChild with
178 ignore (p#replaceChild ~oldChild:f ~newChild:true_child) ;
182 let t' = from#importNode t true in
183 ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
184 (* ignore (highlight_node from t') *)
187 f#get_nodeType,t#get_nodeType
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 ->
196 f#get_namespaceURI,t#get_namespaceURI,f#get_localName,t#get_localName
198 Some nu, Some nu', Some ln, Some ln' when
199 ln#equals ln' && nu#equals nu' ->
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 *)
210 match attr#get_namespaceURI with
212 (* Back to DOM Level 1 ;-( *)
214 let name = attr#get_nodeName in
215 match tattrs#getNamedItem ~name with
217 ignore (fattrs#removeNamedItem ~name)
220 (None,Some name)::!processed ;
221 match attr#get_nodeValue, attr'#get_nodeValue with
222 Some v1, Some v2 when
224 || (name#equals ds_selection &&
225 nu#equals ds_mathmlns &&
226 ln#equals ds_maction)
229 | Some v1, Some v2 ->
230 let attr'' = from#importNode attr' true in
231 ignore (fattrs#setNamedItem attr'')
232 | _,_ -> assert false
234 | Some namespaceURI ->
236 match attr#get_localName with
238 | None -> assert false
241 tattrs#getNamedItemNS ~namespaceURI ~localName
245 (fattrs#removeNamedItemNS
246 ~namespaceURI ~localName)
249 (Some namespaceURI,Some localName)::!processed ;
250 match attr#get_nodeValue, attr'#get_nodeValue with
251 Some v1, Some v2 when
255 let attr'' = from#importNode attr' true in
256 ignore (fattrs#setNamedItem attr'')
257 | _,_ -> assert false
259 for i = 0 to tlen -1 do
260 match tattrs#item i with
263 let namespaceURI,localName =
264 match attr#get_namespaceURI with
266 None,attr#get_nodeName
267 | Some namespaceURI as v ->
268 v, match attr#get_localName with
276 None,Some localName' ->
277 (match namespaceURI with
279 localName#equals localName'
281 | Some namespaceURI', Some localName' ->
282 (match namespaceURI with
284 | Some namespaceURI ->
285 localName#equals localName' &&
286 namespaceURI#equals namespaceURI'
288 | _,_ -> assert false
291 let attr' = from#importNode attr false in
292 ignore (fattrs#setNamedItem attr')
294 | _,_ -> assert false
299 | he1::tl1,he2::tl2 ->
305 let n' = from#importNode n true in
306 ignore (f#appendChild n') ;
307 (* ignore (highlight_node from n') *)
311 List.iter (function n -> ignore (f#removeChild n)) tl1
313 let node_list_of_nodeList n =
318 n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE
319 or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE ->
320 n::(aux n#get_nextSibling)
322 aux n#get_nextSibling
327 (node_list_of_nodeList f, node_list_of_nodeList t)
328 | _,_,_,_ -> replace t1
331 (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) &&
332 (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) ->
334 | _,_ -> assert false
337 aux (d :> Gdome.node)
338 (from#get_documentElement :> Gdome.node)
339 (d#get_documentElement :> Gdome.node)
341 (GdomeInit.DOMException (e,msg) as ex) -> raise ex