X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FTPushParser.cc;fp=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FTPushParser.cc;h=ea82cf379251858d2f9536d56369d98fe513701b;hb=30060cffed61b88fe53e4d6386b606050d6dfda0;hp=0000000000000000000000000000000000000000;hpb=e6927665462cbbace76cff1b17d4f8badcb44eda;p=helm.git diff --git a/helm/DEVEL/mathml_editor/src/TPushParser.cc b/helm/DEVEL/mathml_editor/src/TPushParser.cc new file mode 100644 index 000000000..ea82cf379 --- /dev/null +++ b/helm/DEVEL/mathml_editor/src/TPushParser.cc @@ -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(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); +}