helm/software/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 ;;