X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Ftest%2Fmain.cc;fp=helm%2FDEVEL%2Fmathml_editor%2Ftest%2Fmain.cc;h=3122d529bb469a477dc871e6e157b927165003a1;hp=0000000000000000000000000000000000000000;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hpb=b1fb6b8e1767d775bc452303629e95941d142bea

diff --git a/helm/DEVEL/mathml_editor/test/main.cc b/helm/DEVEL/mathml_editor/test/main.cc
new file mode 100644
index 000000000..3122d529b
--- /dev/null
+++ b/helm/DEVEL/mathml_editor/test/main.cc
@@ -0,0 +1,158 @@
+
+#include "TNode.hh"
+#include "TToken.hh"
+#include "TDocument.hh"
+#include "TPushParser.hh"
+#include "TPushLexer.hh"
+#include "TDictionary.hh"
+#include "TListener.hh"
+#include <GdomeSmartDOMXSLT.hh>
+
+TDictionary dictionary;
+DOM::Document result;
+
+bool
+subst(const DOM::Element& e1, const DOM::GdomeString& id, const DOM::Element& e2)
+{
+  assert(e1);
+  assert(e2);
+  if (e1.getAttribute("xref") == id)
+    {
+      DOM::Node parent = e1.get_parentNode();
+      assert(parent);
+      parent.replaceChild(e2, e1);
+      return true;
+    }
+  else
+    {
+      DOM::Node p = e1.get_firstChild();
+      while (p)
+	{
+	  while (p && p.get_nodeType() != DOM::Node::ELEMENT_NODE) p = p.get_nextSibling();
+	  if (p)
+	    if (subst(p, id, e2)) return true;
+	    else p = p.get_nextSibling();
+	}
+      return false;
+    }
+}
+
+#if 0
+bool
+subst(const DOM::Node& parent, const DOM::GdomeString& id, const DOM::Element& newElem)
+{
+  assert(parent);
+  assert(newElem);
+
+  DOM::Node p = parent.get_firstChild();
+  while (p)
+    {
+      while (p && p.get_nodeType() != DOM::Node::ELEMENT_NODE) p = p.get_nextSibling();
+      if (p)
+	{
+	  DOM::Element el = p;
+	  assert(el);
+	  if (el.getAttribute("xref") == id)
+	    {
+	      parent.replaceChild(el, newElem);
+	      return true;
+	    }
+	  else if (subst(el, id, newElem))
+	    return true;
+	  else
+	    p = p.get_nextSibling();
+	}
+    }
+
+  return false;
+}
+#endif
+
+class MyListener : public TListener
+{
+public:
+  MyListener(const DOM::XSLTStylesheet& s) : style(s) { };
+
+  void callback(TDocument& doc)
+  {
+    TNode dirty = doc.dirtyNode();
+    if (dirty) 
+      {
+	cout << "recreating subtree with id " << std::string(dirty["id"]) << endl;
+	std::vector< std::pair<DOM::GdomeString, DOM::GdomeString> > dirtyId;
+	if (result)
+	  dirtyId.push_back(std::make_pair(DOM::GdomeString("id"),
+					   DOM::GdomeString("'" + std::string(dirty["id"]) + "'")));
+	DOM::Document res = style.apply(doc.document(), dirtyId);
+	assert(res);
+	style.save(res, stdout);
+	if (result)
+	  {
+	    DOM::Element root = res.get_documentElement();
+	    assert(root);
+	    assert(root.hasAttribute("xref"));
+
+	    if (result.get_documentElement().getAttribute("xref") == root.getAttribute("xref"))
+	      {
+		// the following remove should not be necessary
+		// according to the spec replaceChild should work just fine
+		result.removeChild(result.get_documentElement());
+		result.appendChild(result.importNode(root, true));
+	      }
+	    else
+	      try
+		{
+		  cout << "before" << endl;
+		  bool ok = subst(result.get_documentElement(), root.getAttribute("xref"), result.importNode(root, true));
+		  assert(ok);
+		  cout << "after" << endl;
+		}
+	      catch (DOM::DOMException e)
+		{
+		  cerr << "exception " << e.code << " " << e.msg << endl;
+		  assert(0);
+		}
+	  }
+	else
+	  result = res;
+
+	doc.clearDirty();
+      }
+  }
+
+private:
+  const DOM::XSLTStylesheet& style;
+};
+
+main(int argc, char* argv[])
+{
+  if (argc != 2)
+    {
+      cerr << "specify a string, please" << endl;
+      return -1;
+    }
+
+  cout << "loading the dictionary..." << endl;
+  dictionary.load("dictionary.xml");
+
+  cout << "loading the stylesheet..." << endl;
+  DOM::DOMImplementation di;
+  DOM::Document docStyle = di.createDocumentFromURI("./xsl/tml-mmlp.xsl");
+  DOM::XSLTStylesheet style(docStyle);
+  
+  MyListener listener(style);
+  TPushParser parser(dictionary, listener);
+  TPushLexer lexer(parser);
+
+  std::string s = argv[1];
+  for (unsigned long i = 0; i < s.length(); i++)
+    lexer.push(s[i]);
+  lexer.push('\n');
+  
+  cout << "finished" << endl;
+  di.saveDocumentToFile(result, "result.xml", GDOME_SAVE_LIBXML_INDENT);
+
+  cout << "done" << endl;
+
+  parser.document().serialize("output.xml");
+}