helm/gTopLevel/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                 ) tl2
 309             | tl1,[] ->
 310                List.iter (function n -> ignore (f#removeChild n)) tl1
 311           in
 312            let node_list_of_nodeList n =
 313             let rec aux =
 314              function
 315                 None -> []
 316               | Some n when
 317                     n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE
 318                  or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE ->
 319                   n::(aux n#get_nextSibling)
 320               | Some n ->
 321                 aux n#get_nextSibling
 322             in
 323              aux n#get_firstChild
 324            in
 325             dumb_diff
 326              (node_list_of_nodeList f, node_list_of_nodeList t)
 327       | _,_,_,_ -> replace t1
 328       )
 329    | t1,t2 when
 330       (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) &&
 331       (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) ->
 332        replace t1
 333    | _,_ -> assert false
 334  in
 335   try
 336    aux (d :> Gdome.node)
 337     (from#get_documentElement :> Gdome.node)
 338     (d#get_documentElement :> Gdome.node)
 339   with
 340      (GdomeInit.DOMException (e,msg) as ex) -> raise ex
 341   | e -> raise e
 342 ;;