From 75f24bc40a8b7b1d00e6e88cb9a7b08c6551cac7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 22 Jul 2003 14:08:39 +0000 Subject: [PATCH] XmlDiff-ing of DOM trees implemented. SPECIAL FEATURE: the selection attribute of mactions are not patched. --- helm/gTopLevel/.depend | 2 + helm/gTopLevel/Makefile | 13 +- helm/gTopLevel/termViewer.ml | 123 +++++++++++------ helm/gTopLevel/xmlDiff.ml | 248 +++++++++++++++++++++++++++++++++++ helm/gTopLevel/xmlDiff.mli | 26 ++++ 5 files changed, 362 insertions(+), 50 deletions(-) create mode 100644 helm/gTopLevel/xmlDiff.ml create mode 100644 helm/gTopLevel/xmlDiff.mli diff --git a/helm/gTopLevel/.depend b/helm/gTopLevel/.depend index d629a155e..9824aa72a 100644 --- a/helm/gTopLevel/.depend +++ b/helm/gTopLevel/.depend @@ -10,6 +10,8 @@ termEditor.cmi: disambiguate.cmi texTermEditor.cmo: disambiguate.cmi texTermEditor.cmi texTermEditor.cmx: disambiguate.cmx texTermEditor.cmi texTermEditor.cmi: disambiguate.cmi +xmlDiff.cmo: xmlDiff.cmi +xmlDiff.cmx: xmlDiff.cmi termViewer.cmo: logicalOperations.cmi termViewer.cmi termViewer.cmx: logicalOperations.cmx termViewer.cmi invokeTactics.cmo: logicalOperations.cmi proofEngine.cmi termEditor.cmi \ diff --git a/helm/gTopLevel/Makefile b/helm/gTopLevel/Makefile index e44967305..d897036c0 100644 --- a/helm/gTopLevel/Makefile +++ b/helm/gTopLevel/Makefile @@ -21,15 +21,14 @@ DEPOBJS = \ proofEngine.ml proofEngine.mli eta_fixing.ml eta_fixing.mli \ content2cic.ml content2cic.mli logicalOperations.ml \ logicalOperations.mli disambiguate.ml disambiguate.mli termEditor.ml \ - termEditor.mli texTermEditor.ml texTermEditor.mli termViewer.ml \ - termViewer.mli invokeTactics.ml invokeTactics.mli hbugs.ml hbugs.mli \ - gTopLevel.ml + termEditor.mli texTermEditor.ml texTermEditor.mli xmlDiff.ml \ + xmlDiff.mli termViewer.ml termViewer.mli invokeTactics.ml \ + invokeTactics.mli hbugs.ml hbugs.mli gTopLevel.ml TOPLEVELOBJS = \ - eta_fixing.cmo content2cic.cmo \ - proofEngine.cmo logicalOperations.cmo \ - disambiguate.cmo termEditor.cmo texTermEditor.cmo termViewer.cmo \ - invokeTactics.cmo hbugs.cmo gTopLevel.cmo + eta_fixing.cmo content2cic.cmo proofEngine.cmo logicalOperations.cmo \ + disambiguate.cmo termEditor.cmo texTermEditor.cmo xmlDiff.cmo \ + termViewer.cmo invokeTactics.cmo hbugs.cmo gTopLevel.cmo styles: @echo "***********************************************************************" diff --git a/helm/gTopLevel/termViewer.ml b/helm/gTopLevel/termViewer.ml index a54db659d..4f57d80ed 100644 --- a/helm/gTopLevel/termViewer.ml +++ b/helm/gTopLevel/termViewer.ml @@ -150,6 +150,7 @@ class proof_viewer obj = initializer self#set_font_size 10 val mutable current_infos = None + val mutable current_mml = None method make_sequent_of_selected_term = match self#get_selection with @@ -189,57 +190,93 @@ class proof_viewer obj = end | None -> assert false (* "ERROR: No selection!!!" *) - method load_proof uri currentproof = - let - (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, - ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) - = - Cic2acic.acic_object_of_cic_object currentproof - in - if !use_stylesheets then + method load_omdoc_proof uri ~ids_to_inner_sorts cobj = + if !use_stylesheets then + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object (Content2cic.cobj2obj cobj) + in let mml = ApplyStylesheets.mml_of_cic_object ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types in self#load_doc ~dom:mml ; + current_mml <- Some mml ; current_infos <- Some (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; - else - (match acic with - Cic.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> - let time1 = Sys.time () in - let content = - Cic2content.annobj2content - ~ids_to_inner_sorts ~ids_to_inner_types acic in - let pres = Content2pres.content2pres ~ids_to_inner_sorts content in - let time2 = Sys.time () in - (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) - let xmlpres = Mpresentation.print_mpres pres in - let time25 = Sys.time () in - (* - prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); - Xml.pp xmlpres (Some "tmp"); - let time3 = Sys.time () in - prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); - *) - (try - prerr_endline "(******** INIZIO DOM **********)"; - let mml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in - let time3 = Sys.time () in - (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) - prerr_endline "(******** FINE DOM **********)"; - self#load_doc ~dom:mml; - prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2))) - (* - self#load_uri "tmp"; - let time4 = Sys.time () in - prerr_endline - ("Fine loading:" ^ (string_of_float (time4 -. time3))) - *) - with (GdomeInit.DOMException (_,s)) as e -> - prerr_endline s; raise e) - | _ -> assert false); + else +prerr_endline "(******** INIZIO CONTENT ==> PRES **********)"; + let pres = Content2pres.content2pres ~ids_to_inner_sorts cobj in + let time2 = Sys.time () in + (* prerr_endline ("Fine trasformazione:" ^ (string_of_float (time2 -. time1))); *) + let xmlpres = Mpresentation.print_mpres pres in + let time25 = Sys.time () in + (* + prerr_endline ("FINE printing to stream:" ^ (string_of_float (time25 -. time2))); + Xml.pp xmlpres (Some "tmp"); + let time3 = Sys.time () in + prerr_endline ("FINE valutazione e printing dello stream:" ^ (string_of_float (time3 -. time25))); + *) + (try + prerr_endline "(******** INIZIO DOM **********)"; + let mml = Xml2Gdome.document_of_xml Misc.domImpl xmlpres in + let time3 = Sys.time () in + (* ignore (Misc.domImpl#saveDocumentToFile mml "tmp1" ()); *) + prerr_endline "(******** FINE DOM **********)"; + (match current_mml with + None -> + self#load_doc ~dom:mml ; + current_mml <- Some mml + | Some current_mml -> + self#freeze ; +prerr_endline "XML_DIFF: prima passata"; +(* +ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_1.xml" ()) ; +ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_1.xml" ()) ; +*) + XmlDiff.update_dom ~from:current_mml mml ; +(* +prerr_endline "XML_DIFF: seconda passata"; +ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_2.xml" ()) ; +ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_2.xml" ()) ; + XmlDiff.update_dom ~from:current_mml mml ; +ignore (Misc.domImpl#saveDocumentToFile current_mml "/tmp/current_mml_3.xml" ()) ; +ignore (Misc.domImpl#saveDocumentToFile mml "/tmp/mml_3.xml" ()) ; +*) +prerr_endline "XML_DIFF: fine passate"; + self#thaw) ; +(* + self#load_doc ~dom:mml; +*) + prerr_endline ("Fine loading:" ^ (string_of_float (time3 -. time2))) + (* + self#load_uri "tmp"; + let time4 = Sys.time () in + prerr_endline + ("Fine loading:" ^ (string_of_float (time4 -. time3))) + *) + with (GdomeInit.DOMException (_,s)) as e -> + prerr_endline s; raise e) + + method load_proof uri currentproof = + let + (acic,ids_to_terms,ids_to_father_ids,ids_to_inner_sorts, + ids_to_inner_types,ids_to_conjectures,ids_to_hypotheses) + = + Cic2acic.acic_object_of_cic_object currentproof + in + let mml = + ApplyStylesheets.mml_of_cic_object + ~explode_all:true uri acic ids_to_inner_sorts ids_to_inner_types + in + self#load_doc ~dom:mml ; + current_mml <- Some mml ; + current_infos <- + Some + (ids_to_terms,ids_to_father_ids,ids_to_conjectures,ids_to_hypotheses) ; (acic, ids_to_inner_types, ids_to_inner_sorts) end ;; diff --git a/helm/gTopLevel/xmlDiff.ml b/helm/gTopLevel/xmlDiff.ml new file mode 100644 index 000000000..50073f929 --- /dev/null +++ b/helm/gTopLevel/xmlDiff.ml @@ -0,0 +1,248 @@ +(* 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 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 -> assert false + | 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: rimuovo l'attributo " ^ name#to_string); + ignore (f#removeChild attr) + | 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 _, Some _ -> +prerr_endline ("XML_DIFF: DOM 1; rimpiazzo l'attributo " ^ name#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: rimuovo l'attributo " ^ localName#to_string); + ignore (f#removeChild attr) + | 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.0; creo un nuovo attributo " ^ attr#get_nodeName#to_string) ; + None,attr#get_nodeName + | Some namespaceURI as v -> +debugs := ("XML_DIFF: DOM 2.0; 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" ; + List.iter + (function n -> + let n' = from#importNode n true in + ignore (f#appendChild n') + ) tl2 + | tl1,[] -> +prerr_endline "XML_DIFF: cancello i nodi residui" ; + 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"); + 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) -> + let t' = from#importNode t true in +prerr_endline "XML_DIFF: importo il nodo" ; +(* +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) + | _,_,_,_,_,_ -> 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) -> +(* + let module E = GdomeDOMExceptionT in +*) + prerr_endline + ("DOM EXCEPTION: " ^ msg ^ " --- " ^ +string_of_int (Obj.magic e)) ; + raise ex + (* + match e with + E.NO_ERR -> "NO_ERR" + | E.INDEX_SIZE_ERR -> "INDEX_SIZE_ERR" + | E.DOMSTRING_SIZE_ERR -> "DOMSTRING_SIZE_ERR" + | E.HIERARCHY_REQUEST_ERR -> "HIERARCHY_REQUEST_ERR" + | E.WRONG_DOCUMENT_ERR -> "WRONG_DOCUMENT_ERR" + | E.INVALID_CHARACTER_ERR -> "INVALID_CHARACTER_ERR" + | E.NO_DATA_ALLOWED_ERR -> "NO_DATA_ALLOWER_ERR" + | E.NO_MODIFICATION_ALLOWED_ERR -> "NO_MODIFICATION_ALLOWED_ERR" + | E.NOT_FOUND_ERR -> "NOT_FOUND_ERR" + | E.NOT_SUPPORTED_ERR -> "NOT_SUPPORTED_ERR" + | E.INUSE_ATTRIBUTE_ERR -> "INUSE_ATTRIBUTE_ERR" + | E.INVALID_STATE_ERR -> "INVALID_STATE_ERR" + | E.SYNTAX_ERR -> "SYNTAX_ERR" + | E.INVALID_MODIFICATION_ERR -> "INVALID_MODIFICATION_ERR" + | E.NAMESPACE_ERR -> "NAMESPACE_ERR" + | E.INVALID_ACCESS_ERR -> "INVALID_ACCESS_ERR" +*) + | e -> + prerr_endline "PROBLEMA" ; + raise e +;; diff --git a/helm/gTopLevel/xmlDiff.mli b/helm/gTopLevel/xmlDiff.mli new file mode 100644 index 000000000..c62df033b --- /dev/null +++ b/helm/gTopLevel/xmlDiff.mli @@ -0,0 +1,26 @@ +(* 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/. + *) + +val update_dom: from: Gdome.document -> Gdome.document -> unit -- 2.39.2