X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FxmlDiff.ml;fp=helm%2FgTopLevel%2FxmlDiff.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=307e02ac0db8c325fd45b0b5ebb3158a89118a3c;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml deleted file mode 100644 index 307e02ac0..000000000 --- a/helm/gTopLevel/xmlDiff.ml +++ /dev/null @@ -1,394 +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 myprerr_endline = prerr_endline;; -let prerr_endline _ = ();; - -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";; - -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#to_string = mathmlns && ln#to_string = "maction" -> - (new Gdome.element_of_node p)#setAttribute - ~name:(Gdome.domString "selection") - ~value:(Gdome.domString "2") ; - make_visible p - | _,_ -> make_visible p -;; - -let highlight_node ?(color="yellow") (doc: Gdome.document) (n: Gdome.node) = - let highlight (n: Gdome.node) = - let highlighter = - doc#createElementNS - ~namespaceURI:(Some (Gdome.domString mathmlns)) - ~qualifiedName:(Gdome.domString "m:mstyle") - in - highlighter#setAttribute ~name:(Gdome.domString "mathbackground") - ~value:(Gdome.domString color) ; - highlighter#setAttributeNS - ~namespaceURI:(Some (Gdome.domString xmldiffns)) - ~qualifiedName:(Gdome.domString "xmldiff:type") - ~value:(Gdome.domString "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#to_string = mathmlns && - let ln = ln#to_string in - ln <> "mtr" && ln <> "mtd" -> n - | Some nu, Some ln when - nu#to_string = mathmlns && - let ln = ln#to_string in - ln = "mtr" || ln = "mtd" -> -prerr_endline "@@@ find_mstylable_node scendo"; - let true_child = - match n#get_firstChild with - None -> assert false - | Some n -> n - in - find_mstylable_node true_child - | _,_ -> -prerr_endline ("@@@ find_mstylable_node salgo da " ^ match n#get_localName with Some n -> n#to_string | None -> "_") ; - 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 highlight_nodes ~xrefs (doc:Gdome.document) = - let highlighted = ref [] in - let rec aux (n:Gdome.element) = - if - List.mem - (n#getAttributeNS ~namespaceURI:(Gdome.domString helmns) - ~localName:(Gdome.domString "xref"))#to_string - xrefs - then - highlighted := - (highlight_node ~color:"#00ff00"(* light green *) doc (n :> Gdome.node)):: - !highlighted ; - let children = n#get_childNodes in - for i = 0 to children#get_length - 1 do - match children#item i with - None -> assert false - | Some n -> - if n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE then - aux (new Gdome.element_of_node n) - done - 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:(Gdome.domString xmldiffns) - ~localName:(Gdome.domString "type"))#to_string = "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) = -(* Perche' non andava? - if f#get_localName = t#get_localName && - f#get_namespaceURI = t#get_namespaceURI -*) - match - f#get_nodeType,t#get_nodeType, - f#get_namespaceURI,t#get_namespaceURI, - f#get_localName,t#get_localName - with - GdomeNodeTypeT.TEXT_NODE,GdomeNodeTypeT.TEXT_NODE,_,_,_,_ when - match f#get_nodeValue, t#get_nodeValue with - Some v, Some v' -> v#to_string = v'#to_string - | _,_ -> assert false - -> -prerr_endline ("XML_DIFF: preservo il nodo testo " ^ match f#get_nodeValue with Some v -> v#to_string | None -> assert false); - () - | GdomeNodeTypeT.ELEMENT_NODE,GdomeNodeTypeT.ELEMENT_NODE, - Some nu, Some nu', Some ln, Some ln' when - ln#to_string = ln'#to_string && nu#to_string = nu'#to_string -> -prerr_endline ("XML_DIFF: preservo il nodo "^ nu#to_string ^ ":" ^ln#to_string); - 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 -> -prerr_endline ("XML_DIFF: DOM 1; rimuovo l'attributo " ^ name#to_string); -(* CSC: questo non mi toglieva solo l'attributo, ma anche altri nodi qui - e la' ;-( - ignore (f#removeChild attr) -*) - 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#to_string = v2#to_string - || (name#to_string = "selection" && - nu#to_string = - "http://www.w3.org/1998/Math/MathML" && - ln#to_string = "maction") - -> -prerr_endline ("XML_DIFF: DOM 1; preservo l'attributo " ^ name#to_string); - () - | Some v1, Some v2 -> -prerr_endline ("XML_DIFF: DOM 1; rimpiazzo l'attributo " ^ name#to_string ^ ": old value=" ^ v1#to_string ^ ", new value=" ^ v2#to_string); - 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 -> -prerr_endline ("XML_DIFF: DOM 2; rimuovo l'attributo " ^ namespaceURI#to_string ^ ":" ^ localName#to_string); -(* CSC: questo non mi toglieva solo l'attributo, ma anche altri nodi qui - e la' ;-( - ignore (f#removeChild attr) -*) - ignore - (fattrs#removeNamedItemNS - ~namespaceURI ~localName) - | Some attr' -> - processed := - (Some namespaceURI,Some localName)::!processed ; - (*CSC: questo mi dice read-only ;-( - attr#set_nodeValue attr'#get_nodeValue *) - (*CSC: questo mi abortisce con una assert - let attr'' = from#importNode attr' true in - ignore(f#replaceChild ~newChild:attr'' ~oldChild:attr)*) - match attr#get_nodeValue, attr'#get_nodeValue with - Some v1, Some v2 when - v1#to_string = v2#to_string -> -prerr_endline ("XML_DIFF: DOM 2; preservo l'attributo " ^ namespaceURI#to_string ^ ":" ^ localName#to_string); - () - | Some _, Some _ -> -prerr_endline ("XML_DIFF: DOM 2; rimpiazzo l'attributo " ^ namespaceURI#to_string ^ ":" ^ localName#to_string); - 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 debugs = ref "" in - let namespaceURI,localName = - match attr#get_namespaceURI with - None -> -debugs := ("XML_DIFF: DOM 1; creo un nuovo attributo " ^ attr#get_nodeName#to_string) ; - None,attr#get_nodeName - | Some namespaceURI as v -> -debugs := ("XML_DIFF: DOM 2; creo un nuovo attributo " ^ namespaceURI#to_string ^ ":" ^ match attr#get_localName with Some v -> v#to_string | None -> assert false); - 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#to_string = localName'#to_string - | Some _ -> false) - | Some namespaceURI', Some localName' -> - (match namespaceURI with - None -> false - | Some namespaceURI -> - localName#to_string = localName'#to_string && - namespaceURI#to_string=namespaceURI'#to_string - ) - | _,_ -> assert false - ) !processed) - then - let attr' = from#importNode attr false in -prerr_endline !debugs ; - ignore (fattrs#setNamedItem attr') - done - | _,_ -> assert false - end ; - let fchildren = f#get_childNodes in - let tchildren = t#get_childNodes in - let rec dumb_diff = - function - [],[] -> () - | he1::tl1,he2::tl2 -> -prerr_endline "XML_DIFF: processo una coppia di figli" ; - aux f he1 he2 ; - dumb_diff (tl1,tl2) - | [],tl2 -> -prerr_endline ("XML_DIFF: appendo i nodi residui " ^ String.concat ", " (List.map (function n -> match n#get_localName with Some s -> s#to_string | None -> "#" ^ (match n#get_nodeValue with Some s -> s#to_string | None -> "_") ^ "#") tl2)) ; - List.iter - (function n -> - let n' = from#importNode n true in - ignore (f#appendChild n') ; - ignore (highlight_node from n') - ) tl2 - | tl1,[] -> -prerr_endline ("XML_DIFF: cancello i nodi residui " ^ String.concat ", " (List.map (function n -> match n#get_localName with Some s -> s#to_string | None -> "_") tl1)) ; - List.iter (function n -> ignore (f#removeChild n)) tl1 - in - let node_list_of_nodeList nl = - let rec aux i = - match nl#item ~index:i with - None -> [] - | Some n when - n#get_nodeType = GdomeNodeTypeT.ELEMENT_NODE - or n#get_nodeType = GdomeNodeTypeT.TEXT_NODE -> - n::(aux (i+1)) - | Some n -> -prerr_endline ("XML_DIFF: mi sto perdendo i nodi di tipo " ^ string_of_int (Obj.magic n#get_nodeType)) ; - aux (i+1) - in - aux 0 - in -for i = 0 to fchildren#get_length - 1 do -match fchildren#item i with -None -> prerr_endline "EUREKA: ma siamo matti?" -|Some n -> -match n#get_nodeType with GdomeNodeTypeT.ATTRIBUTE_NODE -> prerr_endline "EUREKA attr" | GdomeNodeTypeT.CDATA_SECTION_NODE -> prerr_endline "EUREKA text" | GdomeNodeTypeT.DOCUMENT_FRAGMENT_NODE -> prerr_endline "EUREKA document fragment" | _ -> prerr_endline ("EUREKA " ^ string_of_int (Obj.magic n#get_nodeType)) -done ; -prerr_endline("XML_DIFF: from ha " ^ string_of_int fchildren#get_length ^ " nodi, ovvero " ^ string_of_int (List.length (node_list_of_nodeList fchildren)) ^ " figli"); -prerr_endline("XML_DIFF: to ha " ^ string_of_int tchildren#get_length ^ " nodi, ovvero " ^ string_of_int (List.length (node_list_of_nodeList tchildren)) ^ " figli"); -prerr_endline ("XML_DIFF: chiamo dumb_diff su " ^ String.concat ", " (List.map (function n -> match n#get_localName with Some s -> s#to_string | None -> "_") (node_list_of_nodeList fchildren)) ^ " e " ^ String.concat ", " (List.map (function n -> match n#get_localName with Some s -> s#to_string | None -> "_") (node_list_of_nodeList tchildren))) ; - dumb_diff - (node_list_of_nodeList fchildren, node_list_of_nodeList tchildren) - | t1,t2,_,_,_,_ when - (t1 = GdomeNodeTypeT.ELEMENT_NODE || t1 = GdomeNodeTypeT.TEXT_NODE) && - (t2 = GdomeNodeTypeT.ELEMENT_NODE || t2 = GdomeNodeTypeT.TEXT_NODE) -> - if - t1 = GdomeNodeTypeT.ELEMENT_NODE && - ((new Gdome.element_of_node f)#getAttributeNS - ~namespaceURI:(Gdome.domString xmldiffns) - ~localName:(Gdome.domString "type"))#to_string = "fake" - then - let true_child = - match f#get_firstChild with - None -> assert false - | Some n -> n - in - begin -prerr_endline ("%%% CANCELLO HIGHLIGHTER " ^ (match f#get_localName with Some s -> s#to_string | None -> "_") ^ " CON DENTRO " ^ (match true_child#get_localName with Some s -> s#to_string | None -> "_")) ; - ignore (p#replaceChild ~oldChild:f ~newChild:true_child) ; - aux p true_child t - end - else - let t' = from#importNode t true in -prerr_endline ("%%% XML_DIFF: importo il nodo " ^ match t'#get_localName with Some n -> n#to_string | None -> "_") ; -(* -prerr_endline ("Rimpiazzo" ^ (match f#get_namespaceURI with Some s -> s#to_string) ^ ":" ^ (match f#get_localName with Some s -> s#to_string) ^ " con " ^ (match t#get_namespaceURI with Some s -> s#to_string) ^ ":" ^ (match t#get_localName with Some s -> s#to_string) ^ " in " ^ (match p#get_localName with Some s -> s#to_string | None -> "_")) ; -*) - ignore (p#replaceChild ~newChild:t' ~oldChild:f) ; - ignore (highlight_node from t') - | _,_,_,_,_,_ -> 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) -> -(* CSC: Non si puo' per problemi di linking ;-( - let module E = GdomeDOMExceptionT in -*) - prerr_endline - ("DOM EXCEPTION: " ^ msg ^ " --- " ^ - match e with - GdomeDOMExceptionT.NO_ERR -> "NO_ERR" - | GdomeDOMExceptionT.INDEX_SIZE_ERR -> "INDEX_SIZE_ERR" - | GdomeDOMExceptionT.DOMSTRING_SIZE_ERR -> "DOMSTRING_SIZE_ERR" - | GdomeDOMExceptionT.HIERARCHY_REQUEST_ERR -> "HIERARCHY_REQUEST_ERR" - | GdomeDOMExceptionT.WRONG_DOCUMENT_ERR -> "WRONG_DOCUMENT_ERR" - | GdomeDOMExceptionT.INVALID_CHARACTER_ERR -> "INVALID_CHARACTER_ERR" - | GdomeDOMExceptionT.NO_DATA_ALLOWED_ERR -> "NO_DATA_ALLOWER_ERR" - | GdomeDOMExceptionT.NO_MODIFICATION_ALLOWED_ERR -> "NO_MODIFICATION_ALLOWED_ERR" - | GdomeDOMExceptionT.NOT_FOUND_ERR -> "NOT_FOUND_ERR" - | GdomeDOMExceptionT.NOT_SUPPORTED_ERR -> "NOT_SUPPORTED_ERR" - | GdomeDOMExceptionT.INUSE_ATTRIBUTE_ERR -> "INUSE_ATTRIBUTE_ERR" - | GdomeDOMExceptionT.INVALID_STATE_ERR -> "INVALID_STATE_ERR" - | GdomeDOMExceptionT.SYNTAX_ERR -> "SYNTAX_ERR" - | GdomeDOMExceptionT.INVALID_MODIFICATION_ERR -> "INVALID_MODIFICATION_ERR" - | GdomeDOMExceptionT.NAMESPACE_ERR -> "NAMESPACE_ERR" - | GdomeDOMExceptionT.INVALID_ACCESS_ERR -> "INVALID_ACCESS_ERR") - | e -> - prerr_endline "PROBLEMA" ; - raise e -;;