]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/src/TPushParser.cc
Initial revision
[helm.git] / helm / DEVEL / mathml_editor / src / TPushParser.cc
diff --git a/helm/DEVEL/mathml_editor/src/TPushParser.cc b/helm/DEVEL/mathml_editor/src/TPushParser.cc
new file mode 100644 (file)
index 0000000..ea82cf3
--- /dev/null
@@ -0,0 +1,668 @@
+
+#include "TPushParser.hh"
+#include "TListener.hh"
+
+TPushParser::TPushParser(const TDictionary& d) : dictionary(d), listener(0)
+{
+  init();
+}
+
+TPushParser::TPushParser(const TDictionary& d, TListener& l) : dictionary(d), listener(&l)
+{
+  init();
+}
+
+void
+TPushParser::init()
+{
+  nextId = 1;
+  cursor = doc.create("cursor");
+  cursor["id"] = "I0";
+  doc.clearDirty();
+  doc.root().append(cursor);
+}
+
+TPushParser::~TPushParser()
+{
+}
+
+std::string
+TPushParser::PRIME() const
+{
+  const TDictionary::Entry entry = dictionary.find("prime");
+  if (entry.cls == TDictionary::OPERATOR) return entry.value;
+  else return "?";
+}
+
+void
+TPushParser::do_begin()
+{
+  TNode parent = cursor.parent();
+  if (parent.isC() && dictionary.find(parent.nameC()).table)
+    {
+      TNode row = doc.create("row");
+      TNode cell = doc.create("cell");
+      TNode g = doc.createG();
+      row.append(cell);
+      cell.append(g);
+      g.append(cursor);
+      parent.append(row);
+    }
+  else
+    {
+      TNode g = doc.createG(nextId++);
+      cursor.replace(g);
+      g.append(cursor);
+    }
+}
+
+void
+TPushParser::do_end()
+{
+  TNode parent = cursor.parent();
+  if (parent && parent.isG() && parent.hasId())
+    {
+      // normal closing brace for an explicitly open group
+      cursor.remove();
+      advance(parent);
+    }
+  else if (parent && parent.isG() && parent.parent() && parent.parent().is("cell"))
+    {
+      // closing brace for a structure in which & or \cr have been used
+      TNode row = parent.parent().parent();
+      assert(row && row.is("row"));
+      TNode table = row.parent();
+      assert(table);
+      advance(table);
+    }
+  else if (parent && parent.isG() && !parent.hasId() && parent.parent())
+    {
+      // closing brace for a right-open macro (like \over)
+      cursor.remove();
+      advance(parent.parent());
+    }
+  else
+    {
+      // ???
+      assert(0);
+    }
+}
+
+void
+TPushParser::do_shift()
+{
+  TNode parent = cursor.parent();
+  assert(parent);
+  if (parent.is("tex"))
+    {
+      TNode math = doc.create("math", nextId++);
+      TNode g = doc.createG();
+      cursor.replace(math);
+      math.append(g);
+      g.append(cursor);
+    }
+  else if (parent.isG() && !parent.hasId() && parent.parent() && parent.parent().is("math"))
+    {
+      if (cursor.prev())
+       {
+         // there is something before the cursor, hence this is the
+         // closing math shift
+         if (parent.parent()["display"] != "1")
+           {
+             // one math shift is enough to close it
+             cursor.remove();
+           }
+         else
+           {
+             // we need two closing math shifts
+             parent.parent().append(cursor);
+           }
+       }
+      else if (parent.parent()["display"] != "1")
+       {
+         // there is nothing before the cursor, and the math is not
+         // in display mode, so this must be a double math shift
+         parent.parent()["display"] = "1";
+       }
+      else
+       {
+         parent.parent().append(cursor);
+       }
+    }
+  else if (parent.is("math"))
+    {
+      cursor.remove();
+    }
+  else
+    {
+      cerr << "ERROR: math shift" << endl;
+    }
+}
+
+void
+TPushParser::do_align()
+{
+  TNode parent = cursor.parent();
+  if (parent && parent.isG() && parent.hasId())
+    {
+      // alignment tab used for the first time inside a group
+      TNode row = doc.create("row");
+      TNode cell = doc.create("cell");
+      TNode g = doc.createG();
+      row.append(cell);
+      cell.append(g);
+      g.append(parent.first(), cursor);
+    }
+  else if (parent && parent.isG() && parent.parent().is("cell"))
+    {
+      // alignment tab used within a cell
+      TNode oldCell = parent.parent();
+      assert(oldCell && oldCell.is("cell"));
+      TNode row = oldCell.parent();
+      assert(row && row.is("row"));
+      TNode cell = doc.create("cell");
+      if (oldCell.next()) oldCell.next().insert(cell);
+      else row.append(cell);
+      TNode g = doc.createG();
+      cell.append(g);
+      g.append(cursor);
+    }
+  else
+    {
+      cerr << "alignment tab used outside matrix" << endl;
+    }
+}
+
+void
+TPushParser::do_eol()
+{
+  //if (cursor.parent()) cursor.remove();
+}
+
+void
+TPushParser::do_parameter(const std::string& p)
+{
+  // ???
+}
+
+void
+TPushParser::do_subscript()
+{
+  TNode parent = cursor.parent();
+  if (parent.isG())
+    {
+      TNode prev = cursor.prev();
+      if (!prev)
+       {
+         TNode elem = doc.create("sb", nextId++);
+         TNode g = doc.createG();
+         cursor.replace(elem);
+         elem.append(g);
+         elem.append(cursor);
+       }
+      else
+       {
+         TNode elem = doc.create("sb", nextId++);
+         prev.replace(elem);
+         elem.append(prev);
+         elem.append(cursor);
+       }
+    }
+  else if (parent.isSb() && cursor == parent[1])
+    {
+      if (parent["under"] == "1") cerr << "already under" << endl;
+      else parent["under"] = "1";
+    }
+}
+
+void
+TPushParser::do_superscript()
+{
+  TNode parent = cursor.parent();
+  if (parent.isG())
+    {
+      TNode prev = cursor.prev();
+      if (!prev)
+       {
+         TNode elem = doc.create("sp", nextId++);
+         TNode g = doc.createG();
+         cursor.replace(elem);
+         elem.append(g);
+         elem.append(cursor);
+       }
+      else
+       {
+         TNode elem = doc.create("sp", nextId++);
+         prev.replace(elem);
+         elem.append(prev);
+         elem.append(cursor);
+       }
+    }
+  else if (parent.isSp() && cursor == parent[1])
+    {
+      if (parent["over"] == "1") cerr << "already over" << endl;
+      else parent["over"] = "1";
+    }
+}
+
+void
+TPushParser::do_space(const std::string&)
+{
+  // ? may be used to distinguish tokens in some mode?
+}
+
+void
+TPushParser::do_letter(const std::string& s)
+{
+  TNode parent = cursor.parent();
+  TNode elem = doc.createI(s, nextId++);
+  cursor.replace(elem);
+  advance(elem);
+}
+
+void
+TPushParser::do_digit(const std::string& s)
+{
+  TNode parent = cursor.parent();
+  TNode prev = cursor.prev();
+  if (prev && parent.isG() && prev.is("n"))
+    {
+      TNode elem = doc.createN(prev.value() + s, nextId++);
+      prev.replace(elem);
+    }
+  else
+    {
+      TNode elem = doc.createN(s, nextId++);
+      cursor.replace(elem);
+      advance(elem);
+    }
+}
+
+bool
+TPushParser::isPrimes(const TNode& node) const
+{
+  assert(node);
+  return node.isG() && node.last() && node.last().is("o") && node.last()["val"] == PRIME();
+}
+
+void
+TPushParser::do_apostrophe()
+{
+  if (cursor.parent() && cursor.parent().isG())
+    {
+      if (TNode prev = cursor.prev())
+       {
+         if (prev.isSp() && prev[1] && isPrimes(prev[1]))
+           prev[1].append(doc.createO(PRIME(), nextId++));
+         else if (prev.isSb() && prev[0] &&
+                  prev[0].isSp() && prev[0][1] &&
+                  isPrimes(prev[0][1]))
+           prev[0][1].append(doc.createO(PRIME(), nextId++));
+         else
+           {
+             TNode elem = doc.create("sp");
+             TNode g = doc.createG();
+             prev.replace(elem);
+             elem.append(prev);
+             elem.append(g);
+             g.append(doc.createO(PRIME(), nextId++));
+           }
+       }
+      else
+       {
+         // error ???
+       }
+    }
+  else
+    {
+      // error ??
+    }
+}
+
+void
+TPushParser::do_other(const std::string& s)
+{
+  switch (s[0])
+    {
+    case '\'':
+      do_apostrophe();
+      break;
+    default:
+      cout << "TPushParser::do_other " << s << endl;
+      cout << "DOCUMENT: " << static_cast<GdomeNode*>(cursor.element().get_ownerDocument()) << endl;
+      TNode elem = doc.createT("o", s, nextId++);
+      cursor.replace(elem);
+      advance(elem);  
+      break;
+    }
+}
+
+void
+TPushParser::do_active(const std::string&)
+{
+  // ??? space?
+}
+
+void
+TPushParser::do_comment()
+{
+  // ???
+}
+
+void
+TPushParser::do_cr()
+{
+  TNode parent = cursor.parent();
+  if (parent && parent.isG() &&
+      parent.parent() && parent.parent().is("cell") &&
+      parent.parent().parent() && parent.parent().parent().is("row"))
+    {
+      TNode oldRow = parent.parent().parent();
+      assert(oldRow);
+      TNode table = oldRow.parent();
+      assert(table);
+      TNode row = doc.create("row");
+      TNode cell = doc.create("cell");
+      TNode g = doc.createG();
+      if (oldRow.next()) oldRow.next().insert(row);
+      else table.append(row);
+      row.append(cell);
+      cell.append(g);
+      g.append(cursor);
+    }
+}
+
+void
+TPushParser::do_control(const std::string& name)
+{
+  if (name == "cr") do_cr();
+  else
+    {
+      TNode parent = cursor.parent();
+      const TDictionary::Entry& entry = dictionary.find(name);
+      switch (entry.cls)
+       {
+       case TDictionary::IDENTIFIER:
+         {
+           TNode t = doc.createI(entry.value, nextId++);
+           t["name"] = name;
+           cursor.replace(t);
+           advance(t);
+         }
+         break;
+       case TDictionary::OPERATOR:
+         {
+           TNode t = doc.createO(entry.value, nextId++);
+           t["name"] = name;
+           cursor.replace(t);
+           advance(t);
+         }
+         break;
+       case TDictionary::NUMBER:
+         {
+           TNode t = doc.createN(entry.value, nextId++);
+           t["name"] = name;
+           cursor.replace(t);
+           advance(t);
+         }
+         break;
+       case TDictionary::MACRO:
+         {
+           TNode m = doc.createC(name, nextId++);
+           cursor.replace(m);
+           if (entry.leftOpen && entry.rightOpen)
+             {
+               assert(entry.pattern.empty());
+               assert(parent.isG());
+               TNode g1 = doc.createG();
+               g1["left-open"] = "1";
+               g1.append(parent.first(), m);
+               m.append(g1);
+               TNode g2 = doc.createG();
+               g2.append(cursor);
+               m.append(g2);
+               frames.push(Frame(entry));
+             }
+           else if (entry.leftOpen)
+             {
+               assert(parent.isG());
+               TNode g = doc.createG();
+               g["left-open"] = "1";
+               g.append(parent.first(), m);
+               m.append(g);
+               advance(m);
+             }
+           else if (entry.rightOpen)
+             {
+               assert(entry.pattern.empty());
+               assert(parent.isG());
+               TNode g = doc.createG();
+               g.append(cursor);
+               m.append(g);
+               frames.push(Frame(entry));
+             }
+           else if (!entry.pattern.empty())
+             {
+               if (parent.isG())
+                 {
+                   frames.push(Frame(entry));
+                   if (entry.paramDelimited(0))
+                     {
+                       TNode g = doc.createG();
+                       m.append(g);
+                       g.append(cursor);
+                     }
+                   else
+                     m.append(cursor);
+                 }
+               else
+                 {
+                   // error, but we could handle this very easily
+                   cerr << "error, but we could handle this easily" << endl;
+                 }
+             }
+           else advance(m);
+         }
+         break;
+       case TDictionary::UNDEFINED:
+         {
+           cerr << "ERROR: using undefined macro `" << name << "'" << endl;
+           TNode m = doc.createC(name, nextId++);
+           cursor.replace(m);
+           advance(m);
+         }
+         break;
+       default:
+         assert(0);
+       }
+    }
+}
+
+void
+TPushParser::process(const TToken& token)
+{
+  switch (token.category)
+    {
+    case TToken::BEGIN: do_begin(); break;
+    case TToken::END: do_end(); break;
+    case TToken::SHIFT: do_shift(); break;
+    case TToken::ALIGN: do_align(); break;
+    case TToken::EOL: do_eol(); break;
+    case TToken::PARAMETER: do_parameter(token.value); break;
+    case TToken::SUPERSCRIPT: do_superscript(); break;
+    case TToken::SUBSCRIPT: do_subscript(); break;
+    case TToken::SPACE: do_space(token.value); break;
+    case TToken::LETTER: do_letter(token.value); break;
+    case TToken::DIGIT: do_digit(token.value); break;
+    case TToken::OTHER: do_other(token.value); break;
+    case TToken::ACTIVE: do_active(token.value); break;
+    case TToken::COMMENT: do_comment(); break;
+    case TToken::CONTROL: do_control(token.value); break;
+    }
+}
+
+void
+TPushParser::push(const TToken& token)
+{
+  cerr << "TPushParser::push " << token.value << " (cat: " << token.category << ")" << endl;
+  TNode parent = cursor.parent();
+  // If the cursor has no parent then it is detached from the editing
+  // tree, which means this token will be ignored
+  if (parent)
+    // If the parent is a phantom group and the grand-parent is a
+    // control sequence, there are two cases:
+    // a. we are parsing a delimited argument of a entry
+    // b. we are parsing a side of a right- or left-open entry
+    if (parent.isG() && !parent.hasId() && parent.parent().isC())
+      {
+       // There must be an open frame, for the grand-parent is a control sequence
+       assert(!frames.empty());
+       Frame& frame = frames.top();
+       if (!frame.entry.pattern.empty())
+         {
+           // The entry pattern is not empty. By our conventions this means
+           // the entry cannot be open at either end, hence we are parsing
+           // a delimited argument
+           assert(frame.pos + 1 < frame.entry.pattern.size());
+           assert(frame.entry.pattern[frame.pos + 1].category != TToken::PARAMETER);
+           if (frame.entry.pattern[frame.pos + 1] == token)
+             {
+               // The token matches with the delimiter of the argument.
+               cursor.remove();
+
+               // If the phantom group has just one child, it is not necessary
+               // and can be removed. However, this would complicate
+               // all the code that follows, so given it is a rare case we
+               // leave it alone
+               // if (parent.size() == 1) parent.replace(parent[0]);
+
+               // Eat both the argument and its delimiter
+               frame.pos += 2;
+               if (frame.pos == frame.entry.pattern.size())
+                 {
+                   // This token has completed the entry
+                   advance(parent.parent());
+                 }
+               else if (frame.entry.paramDelimited(frame.pos))
+                 {
+                   // For the next is a delimited argument we have to place
+                   // a suitable phantom group with the cursor inside
+                   TNode g = doc.createG();
+                   parent.parent().append(g);
+                   g.append(cursor);
+                 }
+               else
+                 parent.parent().append(cursor);
+             }
+           else
+             {
+               // Delimiter mismatch. Since we are parsing a delimited
+               // argument we just process the token
+               process(token);
+             }
+         }
+       else
+         {
+           // The entry pattern is empty, hence we are parsing a right-open
+           // entry. What happens if we actually are in the left side?
+           // This could happen only when re-editing an entered expression
+           // We'll see...
+           assert(frame.entry.rightOpen);
+           process(token);
+         }
+      }
+    else if (parent.isC())
+      {
+       // We are parsing a non-delimited argument entry
+       // or a fixed token
+       Frame& frame = frames.top();
+       assert(frame.pos < frame.entry.pattern.size());
+       if (frame.entry.pattern[frame.pos].category == TToken::PARAMETER)
+         {
+           // As by the TeX parsing rules of undelimited parameters,
+           // empty spaces are ignored
+           if (token.category != TToken::SPACE)
+             {
+               // We need to increase the frame position here, becase inside
+               // process the function advance will be called. At that point
+               // it will be important for the parser to know that the entry
+               // has been completed in order to place the cursor correctly
+               // in the next position
+               frame.pos++;
+               process(token);
+             }
+         }
+       else if (frame.entry.pattern[frame.pos] == token)
+         {
+           // The token has been accepted
+           frame.pos++;
+           if (frame.pos < frame.entry.pattern.size() &&
+               frame.entry.paramDelimited(frame.pos))
+             {
+               // If the next is a delimited argument we have to place
+               // the phantom group with the cursor inside
+               TNode g = doc.createG();
+               cursor.replace(g);
+               g.append(cursor);
+             }
+           else
+             advance(parent);
+         }
+       else
+         {
+           // There is a mismatch. Emit an error and ignore the token?
+           cerr << "ERROR: token ignored: " << token.value << " (cat: " << token.category << ")" << endl;
+         }
+
+      }
+    else
+      process(token);
+  else
+    {
+      cout << "ignored token" << endl;
+    }
+
+  if (listener) listener->callback(doc);
+}
+
+void
+TPushParser::advance(const TNode& node)
+{
+  assert(node);
+  TNode parent = node.parent();
+  if (!parent)
+    ; // nothing to do, the cursor is not in the document any more
+  else if (parent.isG())
+    {
+      TNode next = node.next();
+      if (next) next.insert(cursor);
+      else parent.append(cursor);
+    }
+  else if (parent.isC())
+    {
+      if (node.next())
+       ; // cursor removed
+      else
+       {
+         Frame& frame = frames.top();
+         if (frame.pos == frame.entry.pattern.size())
+           {
+             frames.pop();
+             advance(parent);
+           }
+         else
+           parent.append(cursor);
+       }
+    }
+  else if (parent.is("math"))
+    ; // we are done
+  else
+    advance(parent);
+}
+
+void
+TPushParser::setCursor(const std::string& c)
+{
+  cursor["val"] = c;
+  if (listener) listener->callback(doc);
+}