X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FDiff.cc;fp=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FDiff.cc;h=948baa6b6e10e6b4b7607260076dc4394d2bbbc6;hb=387aeebf96181c051b7f527a0901b173cfcdf194;hp=0000000000000000000000000000000000000000;hpb=2f94240bc382ca43017f31b0852f1717fe18090b;p=helm.git diff --git a/helm/DEVEL/mathml_editor/src/Diff.cc b/helm/DEVEL/mathml_editor/src/Diff.cc new file mode 100644 index 000000000..948baa6b6 --- /dev/null +++ b/helm/DEVEL/mathml_editor/src/Diff.cc @@ -0,0 +1,368 @@ + +#include +#include +#include +#include + +#include "Diff.hh" + +namespace GdomeSmartDOMExt +{ + + Diff + Diff::diff(const Document& dest, const Document& source, flatNodeEq flatEq) + { + assert(dest); + assert(source); + assert(flatEq); + + return diff(dest.get_documentElement(), source.get_documentElement(), flatEq); + } + + Diff + Diff::diff(const Element& dest, const Element& source, flatNodeEq flatEq) + { + assert(dest); + assert(source); + assert(flatEq); + + DOMImplementation di; + Document doc = di.createDocument(DDIFF_NS_URI, "diff:doc", DocumentType()); + Element root = doc.get_documentElement(); + root.setAttributeNS(XMLNS_NS_URI, "xmlns:diff", DDIFF_NS_URI); + + Diff diff(dest, doc, flatEq); + if (Node d = diff.diffNodes(dest, source)) root.appendChild(d); + else root.appendChild(doc.createElementNS(DDIFF_NS_URI, "diff:same")); + + return diff; + } + + struct NodeEqPredicate : std::binary_function + { + NodeEqPredicate(Diff::flatNodeEq e) : eq(e) { }; + bool operator()(const Node& n1, const Node& n2) const { return eq(n1, n2); }; + + private: + Diff::flatNodeEq eq; + }; + + std::vector + collectProperAttributes(const Node& n) + { + assert(n); + NamedNodeMap map = n.get_attributes(); + unsigned len = map.get_length(); + + std::vector res; + res.reserve(len); + for (unsigned i = 0; i < len; i++) + { + Node attr = map.item(i); + assert(attr); + if (attr.get_nodeName() != "xmlns" && attr.get_prefix() != "xmlns") res.push_back(attr); + } + + return res; + } + + bool + Diff::defaultFlatNodeEq(const Node& n1, const Node& n2) + { + assert(n1); + assert(n2); + + unsigned nodeType = n1.get_nodeType(); + if (nodeType != n2.get_nodeType()) return false; + + GdomeString ns1 = n1.get_namespaceURI(); + GdomeString ns2 = n2.get_namespaceURI(); + if (ns1 != ns2) return false; + + switch (nodeType) + { + case Node::ATTRIBUTE_NODE: + if (!ns1.null()) + { + assert(!ns2.null()); + if (n1.get_localName() != n2.get_localName()) return false; + } + else + { + assert(ns2.null()); + if (n1.get_nodeName() != n2.get_nodeName()) return false; + } + // WARNING: fallback for checking node value + case Node::TEXT_NODE: + case Node::CDATA_SECTION_NODE: + if (n1.get_nodeValue() != n2.get_nodeValue()) return false; + return true; + case Node::ELEMENT_NODE: + { + //cout << "comparing: " << n1.get_nodeName() << " ? " << n2.get_nodeName() << endl; + if (!ns1.null()) + { + assert(!ns2.null()); + if (n1.get_localName() != n2.get_localName()) return false; + } + else + { + assert(ns2.null()); + if (n1.get_nodeName() != n2.get_nodeName()) return false; + } +#if 1 + std::vector m1 = collectProperAttributes(n1); + std::vector m2 = collectProperAttributes(n2); + if (m1.size() != m2.size()) return false; + + for (unsigned i = 0; i < m1.size(); i++) + { + std::vector::iterator p2 = std::find_if(m2.begin(), m2.end(), std::bind2nd(NodeEqPredicate(defaultFlatNodeEq), m1[i])); + if (p2 == m2.end()) return false; + } +#endif + } + return true; + default: + return true; + } + + } + + void + Diff::sameChunk(const Node& res, unsigned long n) const + { + assert(n > 0); + Element s = doc.createElementNS(DDIFF_NS_URI, "diff:same"); + if (n != 1) + { + std::ostringstream os; + os << n; + s.setAttribute("count", os.str()); + } + res.appendChild(s); + } + + Node + Diff::diffNodes(const Node& p1, const Node& p2) const + { + if (eq(p1, p2)) + { + Element m = doc.createElementNS(DDIFF_NS_URI, "diff:merge"); + if (diffChildren(p1, p2, m)) return m; + else return Node(); + } + else + { + Element r = doc.createElementNS(DDIFF_NS_URI, "diff:replace"); + r.appendChild(doc.importNode(p2, true)); + return r; + } + } + + bool + Diff::diffChildren(const Node& n1, const Node& n2, const Node& res) const + { + assert(n1); + assert(n2); + assert(res); + + Node p1 = n1.get_firstChild(); + Node p2 = n2.get_firstChild(); + bool same = true; + unsigned nSame = 0; + while (p1 && p2) + { + if (Node d = diffNodes(p1, p2)) + { + same = false; + if (nSame > 0) + { + sameChunk(res, nSame); + nSame = 0; + } + res.appendChild(d); + } + else + nSame++; + + p1 = p1.get_nextSibling(); + p2 = p2.get_nextSibling(); + } + + if (p1) + { + same = false; + if (nSame > 0) + { + sameChunk(res, nSame); + nSame = 0; + } + + unsigned nRemoved = 0; + while (p1) + { + nRemoved++; + p1 = p1.get_nextSibling(); + } + + if (nRemoved > 0) + { + Element r = doc.createElementNS(DDIFF_NS_URI, "diff:remove"); + if (nRemoved > 1) + { + std::ostringstream os; + os << nRemoved; + r.setAttribute("count", os.str()); + } + res.appendChild(r); + } + } + + if (p2) + { + same = false; + if (nSame > 0) + { + sameChunk(res, nSame); + nSame = 0; + } + + Element i = doc.createElementNS(DDIFF_NS_URI, "diff:insert"); + while (p2) + { + i.appendChild(doc.importNode(p2, true)); + p2 = p2.get_nextSibling(); + } + res.appendChild(i); + } + + return !same; + } + + static Node + getFirstElement(const Node& n) + { + Node p = n.get_firstChild(); + while (p && p.get_nodeType() != Node::ELEMENT_NODE) + p = p.get_nextSibling(); + return p; + } + + static Node + getNextElement(const Node& n) + { + Node p = n.get_nextSibling(); + while (p && p.get_nodeType() != Node::ELEMENT_NODE) + p = p.get_nextSibling(); + return p; + } + + void + Diff::patchRootNode(const Node& node, const Element& elem) const + { + GdomeString name = elem.get_localName(); + if (name == "same") + { + if (elem.hasAttribute("count")) + { + unsigned count; + istringstream is(elem.getAttribute("count")); + is >> count; + assert(count == 1); + } + } + else if (name == "replace") + { + Document d1 = node.get_ownerDocument(); + Node parent = node.get_parentNode(); + assert(parent); +#if 0 + /* the following patch is because of gdome2 bug that prevents from + * replacing the root element of a document. + */ + assert(!node.get_previousSibling()); + assert(!node.get_nextSibling()); + parent.removeChild(node); + parent.appendChild(d1.importNode(getFirstElement(elem), true)); +#endif + parent.replaceChild(d1.importNode(getFirstElement(elem), true), node); + } + else if (name == "merge") + patchChildren(node, elem); + else + assert(0); + } + + void + Diff::patchChildren(const Node& n1, const Element& e2) const + { + Node p1 = n1.get_firstChild(); + Element p2 = getFirstElement(e2); + while (p2) + { + GdomeString name = p2.get_localName(); + if (name == "same") + { + unsigned count = 1; + if (p2.hasAttribute("count")) + { + istringstream is(p2.getAttribute("count")); + is >> count; + } + while (count-- > 0) + { + if (!p1) throw BADDiff("too few nodes in original document (same)"); + p1 = p1.get_nextSibling(); + } + } + else if (name == "replace") + { + Document d1 = n1.get_ownerDocument(); + if (!p1) throw BADDiff("no node to replace in original document"); + Node next = p1.get_nextSibling(); + n1.replaceChild(d1.importNode(p2.get_firstChild(), true), p1); + p1 = next; + } + else if (name == "insert") + { + Document d1 = n1.get_ownerDocument(); + for (Node i = p2.get_firstChild(); i; i = i.get_nextSibling()) + n1.insertBefore(d1.importNode(i, true), p1); + } + else if (name == "merge") + { + if (!p1) throw BADDiff("no node to merge in original document"); + patchChildren(p1, p2); + p1 = p1.get_nextSibling(); + } + else if (name == "remove") + { + unsigned count = 1; + if (p2.hasAttribute("count")) + { + istringstream is(p2.getAttribute("count")); + is >> count; + } + while (count-- > 0) + { + if (!p1) throw BADDiff("too few nodes in original document (remove)"); + Node next = p1.get_nextSibling(); + n1.removeChild(p1); + p1 = next; + } + } + else + assert(0); + + p2 = getNextElement(p2); + } + } + + void + Diff::patch() const + { + patchRootNode(dest, getFirstElement(doc.get_documentElement())); + } + +}