]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/gTopLevel/xmlDiff.ml
This commit was manufactured by cvs2svn to create branch 'moogle'.
[helm.git] / helm / gTopLevel / xmlDiff.ml
diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml
deleted file mode 100644 (file)
index cd19beb..0000000
+++ /dev/null
@@ -1,342 +0,0 @@
-(* Copyright (C) 2000-2002, HELM Team.
- * 
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- * 
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- * 
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA  02111-1307, USA.
- * 
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-let mathmlns = "http://www.w3.org/1998/Math/MathML";;
-let xmldiffns = "http://helm.cs.unibo.it/XmlDiff";;
-let helmns = "http://www.cs.unibo.it/helm";;
-
-let ds_selection      = Gdome.domString "selection";;
-let ds_2              = Gdome.domString "2";;
-let ds_mathmlns       = Gdome.domString mathmlns;;
-let ds_m_style        = Gdome.domString "m:mstyle";;
-let ds_mathbackground = Gdome.domString "mathbackground";;
-let ds_xmldiffns      = Gdome.domString xmldiffns;;
-let ds_xmldiff_type   = Gdome.domString "xmldiff:type";;
-let ds_fake           = Gdome.domString "fake";;
-let ds_helmns         = Gdome.domString helmns;;
-let ds_xref           = Gdome.domString "xref";;
-let ds_type           = Gdome.domString "type";;
-let ds_yellow         = Gdome.domString "yellow";;
-let ds_green          = Gdome.domString "#00ff00";;
-let ds_maction        = Gdome.domString "maction";;
-let ds_mtr            = Gdome.domString "mtr";;
-let ds_mtd            = Gdome.domString "mtd";;
-
-type highlighted_nodes = Gdome.node list;;
-
-let rec make_visible (n: Gdome.node) =
- match n#get_parentNode with
-    None -> ()
-  | Some p ->
-     match p#get_namespaceURI, p#get_localName with
-        Some nu, Some ln when
-         nu#equals ds_mathmlns && ln#equals ds_maction ->
-          (new Gdome.element_of_node p)#setAttribute
-            ~name:ds_selection
-             ~value:ds_2 ;
-          make_visible p
-      | _,_ -> make_visible p
-;;
-
-let highlight_node_total_time = ref 0.0;;
-
-let highlight_node ?(color=ds_yellow) (doc: Gdome.document) (n: Gdome.node) =
- let highlight (n: Gdome.node) =
-  let highlighter =
-   doc#createElementNS
-    ~namespaceURI:(Some ds_mathmlns)
-    ~qualifiedName:ds_m_style
-  in
-   highlighter#setAttribute ~name:ds_mathbackground ~value:color ;
-   highlighter#setAttributeNS
-    ~namespaceURI:(Some ds_xmldiffns)
-    ~qualifiedName:ds_xmldiff_type
-    ~value:ds_fake ;
-   let parent = 
-    match n#get_parentNode with
-       None -> assert false
-     | Some p -> p
-   in
-    ignore
-     (parent#replaceChild ~oldChild:n ~newChild:(highlighter :> Gdome.node)) ;
-    ignore (highlighter#appendChild n) ;
-    (highlighter :> Gdome.node)
- in
-  let rec find_mstylable_node n =
-   match n#get_namespaceURI, n#get_localName with
-      Some nu, Some ln when
-       nu#equals ds_mathmlns &&
-        (not (ln#equals ds_mtr)) && (not (ln#equals ds_mtd)) -> n
-    | Some nu, Some ln when
-       nu#equals ds_mathmlns &&
-        ln#equals ds_mtr || ln#equals ds_mtd ->
-         let true_child =
-          match n#get_firstChild with
-             None -> assert false
-           | Some n -> n
-         in
-          find_mstylable_node true_child
-    | _,_ ->
-      match n#get_parentNode with
-         None -> assert false
-       | Some p -> find_mstylable_node p
-  in
-   let highlighter = highlight (find_mstylable_node n) in
-    make_visible highlighter ;
-    highlighter
-;;
-
-let iter_children ~f (n:Gdome.node) =
- let rec aux =
-  function
-     None -> ()
-   | Some n ->
-      let sibling = n#get_nextSibling in
-       (f n) ;
-       aux sibling
- in
-  aux n#get_firstChild
-;;
-
-let highlight_nodes ~xrefs (doc:Gdome.document) =
- let highlighted = ref [] in
- let rec aux (n:Gdome.element) =
-  let attributeNS =
-    (n#getAttributeNS ~namespaceURI:ds_helmns
-     ~localName:ds_xref)#to_string in
-  if List.mem attributeNS xrefs then
-   highlighted :=
-    (highlight_node ~color:ds_green doc (n :> Gdome.node))::
-    !highlighted ;
-   iter_children (n :> Gdome.node)
-    ~f:(function n ->
-         if n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE then
-          aux (new Gdome.element_of_node n))
- in
-  aux doc#get_documentElement ;
-  !highlighted
-;;
-
-let dim_nodes =
- List.iter 
-  (function (n : Gdome.node) ->
-    assert
-     (n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE &&
-      ((new Gdome.element_of_node n)#getAttributeNS
-        ~namespaceURI:ds_xmldiffns
-        ~localName:ds_type)#equals ds_fake) ;
-    let true_child =
-     match n#get_firstChild with
-        None -> assert false
-      | Some n -> n in
-    let p =
-     match n#get_parentNode with
-        None -> assert false
-      | Some n -> n
-    in
-     ignore (p#replaceChild ~oldChild:n ~newChild:true_child)
-  )
-;;
-
-let update_dom ~(from : Gdome.document) (d : Gdome.document) =
- let rec aux (p: Gdome.node) (f: Gdome.node) (t: Gdome.node) =
- let replace t1 =
-  if
-   t1 = GdomeNodeTypeT.ELEMENT_NODE &&
-   ((new Gdome.element_of_node f)#getAttributeNS
-     ~namespaceURI:ds_xmldiffns
-     ~localName:ds_type)#equals ds_fake
-  then
-   let true_child =
-    match f#get_firstChild with
-       None -> assert false
-     | Some n -> n
-   in
-    begin
-     ignore (p#replaceChild ~oldChild:f ~newChild:true_child) ;
-     aux p true_child t
-    end
-  else
-   let t' = from#importNode t true in
-    ignore (p#replaceChild ~newChild:t' ~oldChild:f) ;
-    ignore (highlight_node from t')
-  in
-  match
-   f#get_nodeType,t#get_nodeType
-  with
-     GdomeNodeTypeT.TEXT_NODE,GdomeNodeTypeT.TEXT_NODE ->
-      (match f#get_nodeValue, t#get_nodeValue with
-          Some v, Some v' when v#equals v' -> ()
-        | Some _, (Some _ as v') -> f#set_nodeValue v'
-        | _,_ -> assert false)
-   | GdomeNodeTypeT.ELEMENT_NODE as t1,GdomeNodeTypeT.ELEMENT_NODE ->
-      (match
-        f#get_namespaceURI,t#get_namespaceURI,f#get_localName,t#get_localName
-       with
-        Some nu, Some nu', Some ln, Some ln' when
-         ln#equals ln' && nu#equals nu' ->
-          begin
-           match f#get_attributes, t#get_attributes with
-              Some fattrs, Some tattrs ->
-               let flen = fattrs#get_length in
-               let tlen = tattrs#get_length in
-                let processed = ref [] in
-                for i = 0 to flen -1 do
-                 match fattrs#item i with
-                    None -> () (* CSC: sigh, togliere un nodo rompe fa decrescere la lunghezza ==> passare a un while *)
-                  | Some attr ->
-                      match attr#get_namespaceURI with
-                         None ->
-                          (* Back to DOM Level 1 ;-( *)
-                          begin
-                           let name = attr#get_nodeName in
-                            match tattrs#getNamedItem ~name with
-                               None ->
-                               ignore (fattrs#removeNamedItem ~name)
-                             | Some attr' ->
-                                processed :=
-                                 (None,Some name)::!processed ;
-                                match attr#get_nodeValue, attr'#get_nodeValue with
-                                   Some v1, Some v2 when
-                                       v1#equals v2
-                                    || (name#equals ds_selection &&
-                                        nu#equals ds_mathmlns &&
-                                        ln#equals ds_maction)
-                                    ->
-                                     ()
-                                 | Some v1, Some v2 ->
-                                    let attr'' = from#importNode attr' true in
-                                     ignore (fattrs#setNamedItem attr'')
-                                 | _,_ -> assert false
-                          end
-                       | Some namespaceURI ->
-                          let localName = 
-                           match attr#get_localName with
-                             Some v -> v
-                            | None -> assert false
-                          in
-                           match
-                            tattrs#getNamedItemNS ~namespaceURI ~localName
-                           with
-                              None ->
-                               ignore
-                                (fattrs#removeNamedItemNS
-                                  ~namespaceURI ~localName)
-                            | Some attr' ->
-                               processed :=
-                                (Some namespaceURI,Some localName)::!processed ;
-                                match attr#get_nodeValue, attr'#get_nodeValue with
-                                   Some v1, Some v2 when
-                                    v1#equals v2 ->
-                                     ()
-                                 | Some _, Some _ ->
-                                    let attr'' = from#importNode attr' true in
-                                     ignore (fattrs#setNamedItem attr'')
-                                 | _,_ -> assert false
-                done ;
-                for i = 0 to tlen -1 do
-                 match tattrs#item i with
-                    None -> assert false
-                  | Some attr ->
-                     let namespaceURI,localName =
-                      match attr#get_namespaceURI with
-                         None ->
-                          None,attr#get_nodeName
-                       | Some namespaceURI as v ->
-                         v, match attr#get_localName with
-                            None -> assert false
-                          | Some v -> v
-                     in
-                      if
-                       not
-                        (List.exists
-                          (function
-                              None,Some localName' ->
-                               (match namespaceURI with
-                                   None ->
-                                    localName#equals localName'
-                                 | Some _ -> false)
-                            | Some namespaceURI', Some localName' ->
-                               (match namespaceURI with
-                                   None -> false
-                                 | Some namespaceURI ->
-                                    localName#equals localName' &&
-                                    namespaceURI#equals namespaceURI'
-                               )
-                            | _,_ -> assert false
-                          ) !processed)
-                      then
-                       let attr' = from#importNode attr false in
-                        ignore (fattrs#setNamedItem attr')
-                done
-            | _,_ -> assert false
-          end ;
-          let rec dumb_diff =
-           function
-              [],[] -> ()
-            | he1::tl1,he2::tl2 ->
-               aux f he1 he2 ;
-               dumb_diff (tl1,tl2)
-            | [],tl2 ->
-               List.iter
-                (function n ->
-                  let n' = from#importNode n true in
-                    ignore (f#appendChild n') ;
-                    ignore (highlight_node from n')
-                ) tl2
-            | tl1,[] ->
-               List.iter (function n -> ignore (f#removeChild n)) tl1
-          in
-           let node_list_of_nodeList n =
-            let rec aux =
-             function
-                None -> []
-              | Some n when
-                    n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE
-                 or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE ->
-                  n::(aux n#get_nextSibling)
-              | Some n ->
-                aux n#get_nextSibling
-            in
-             aux n#get_firstChild
-           in
-            dumb_diff
-             (node_list_of_nodeList f, node_list_of_nodeList t)
-      | _,_,_,_ -> replace t1
-      )
-   | t1,t2 when
-      (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) &&
-      (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) ->
-       replace t1
-   | _,_ -> assert false
- in
-  try
-   aux (d :> Gdome.node)
-    (from#get_documentElement :> Gdome.node)
-    (d#get_documentElement :> Gdome.node)
-  with
-     (GdomeInit.DOMException (e,msg) as ex) -> raise ex
-  | e -> raise e
-;;