X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FTDictionary.cc;h=3cf2334876ded1f66367a302c558675c6c017f51;hb=1957a1f151c547f04625c4379e51ab66bddb69c7;hp=dcaf1d627562f072f8a535fe1a8f62a6edb226fb;hpb=bf29ef82dc843dcb1929b413b36801ac26441fbd;p=helm.git

diff --git a/helm/DEVEL/mathml_editor/src/TDictionary.cc b/helm/DEVEL/mathml_editor/src/TDictionary.cc
index dcaf1d627..3cf233487 100644
--- a/helm/DEVEL/mathml_editor/src/TDictionary.cc
+++ b/helm/DEVEL/mathml_editor/src/TDictionary.cc
@@ -4,24 +4,44 @@
 #include "dom.hh"
 #include "TDictionary.hh"
 #include "TTokenizer.hh"
+#include "CLoggerConsole.hh"
 
 static TDictionary::Entry undefinedEntry;
 
 void
-TDictionary::load(const char* uri)
+TDictionary::load(const std::string& uri)
 {
+  logger.debug("Dictionary: loading `" + uri + "'");
+
   DOM::DOMImplementation di;
+  DOM::Document doc = di.createDocumentFromURI(uri.c_str());
+  assert(doc);
+  load(doc);
+}
 
-  DOM::Document doc = di.createDocumentFromURI(uri);
+void
+TDictionary::load(const DOM::Document& doc)
+{
   assert(doc);
 
   DOM::Element root = doc.get_documentElement();
   assert(root);
 
-  TTokenizer tokenizer;
+  CLoggerConsole logger;
+  TTokenizer tokenizer(logger);
 
   for (DOM::Node p = root.get_firstChild(); p; p = p.get_nextSibling())
-    if (p.get_nodeType() == DOM::Node::ELEMENT_NODE && p.get_nodeName() == "entry")
+    if (p.get_nodeType() == DOM::Node::ELEMENT_NODE && p.get_nodeName() == "include")
+      {
+	DOM::Element el = p;
+	assert(el);
+	if (el.hasAttribute("href"))
+	  // WARNING: this may result into an infinite loop!
+	  load(std::string(el.getAttribute("href")));
+	else
+	  logger.warning("Dictionary: include statement with no href attribute (ignored)");
+      }
+    else if (p.get_nodeType() == DOM::Node::ELEMENT_NODE && p.get_nodeName() == "entry")
       {
 	DOM::Element el = p;
 	assert(el);
@@ -29,7 +49,7 @@ TDictionary::load(const char* uri)
 
 	std::string name = el.getAttribute("name");
 	if (entries.find(name) != entries.end())
-	  cerr << "WARNING: entry `" << name << "' is being redefined" << endl;
+	  logger.info("Dictionary: `" + name + "' is being redefined");
 
 	Entry entry;
 
@@ -48,13 +68,13 @@ TDictionary::load(const char* uri)
 	  {
 	    entry.value = el.getAttribute("val");
 	    if (entry.cls == MACRO)
-	      cerr << "WARNING: `" << name << "' has a specified value, but is classified as macro" << endl;
+	      logger.warning("Dictionary: `" + name + "' has a specified value, but is classified as macro");
 	  }
 
 	if (el.hasAttribute("pattern"))
 	  {
 	    if (entry.cls != MACRO)
-	      cerr << "WARNING: `" << name << "' has a specified pattern, but is not classified as macro" << endl;
+	      logger.warning("Dictionary: `" + name + "' has a specified pattern, but is not classified as macro");
 
 	    std::string pattern = el.getAttribute("pattern");
 	    if (pattern == "{}")
@@ -67,6 +87,7 @@ TDictionary::load(const char* uri)
 	      entry.pattern = tokenizer.tokenize(pattern);
 	  }
 
+#if 0
 	if (el.hasAttribute("infix"))
 	  {
 	    std::istringstream is(el.getAttribute("infix"));
@@ -102,6 +123,7 @@ TDictionary::load(const char* uri)
 		if (!el.hasAttribute("prefix")) entry.prefix = postfix;
 	      }
 	  }
+#endif
 
 	if (el.hasAttribute("limits"))
 	  {
@@ -122,7 +144,7 @@ TDictionary::load(const char* uri)
 	if (el.hasAttribute("delimiter"))
 	  {
 	    if (entry.cls != OPERATOR && !entry.embellishment)
-	      cerr << "WARNING: `" << name << "' delimiter ignored for non-operator" << endl;
+	      logger.warning("Dictionary: `" + name + "' delimiter ignored for non-operator");
 
 	    std::istringstream is(el.getAttribute("delimiter"));
 	    unsigned delimiter;
@@ -133,7 +155,7 @@ TDictionary::load(const char* uri)
 	if (el.hasAttribute("table"))
 	  {
 	    if (entry.cls != MACRO)
-	      cerr << "WARNING: `" << name << "' table ignored for non-macro" << endl;
+	      logger.warning("Dictionary: `" + name + "' table ignored for non-macro");
 
 	    std::istringstream is(el.getAttribute("table"));
 	    unsigned table;