]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/DEVEL/mathml_editor/src/TPushParser.cc
ocaml 3.09 transition
[helm.git] / helm / DEVEL / mathml_editor / src / TPushParser.cc
index 863ca7bb06e4e1bfb2e956036605e31ee76b7a87..0c96fe43968c94be52a1fdcffac385012d683ebb 100644 (file)
@@ -23,6 +23,8 @@
  * or send an email to <lpadovan@cs.unibo.it>
  */
 
+#include <cassert>
+
 #include "ALogger.hh"
 #include "TPushParser.hh"
 #include "AMathMLFactory.hh"
@@ -55,9 +57,10 @@ TPushParser::reset()
 {
   nextId = 1;
   if (cursor.parent()) cursor.remove();
+  cursor["val"] = "";
   doc.reset();
   doc.root().append(cursor);
-  if (factory) factory->documentModified(doc);
+  if (factory && !frozen()) factory->documentModified(doc);
 }
 
 TNode
@@ -214,7 +217,7 @@ TPushParser::do_end()
            }
          else
            {
-             logger.warning("closing brace ignored");
+             logger.warning("ignored closing brace");
              return false;
            }
        }
@@ -290,7 +293,7 @@ TPushParser::do_shift()
     }
   else
     {
-      logger.warning("parser: math shift");
+      logger.warning("not allowed here");
       return false;
     }
 }
@@ -336,14 +339,14 @@ bool
 TPushParser::do_eol()
 {
   //if (cursor.parent()) cursor.remove();
-  logger.warning("token ignored");
+  logger.warning("ignored token");
   return false;
 }
 
 bool
 TPushParser::do_parameter(const std::string& p)
 {
-  logger.warning("token ignored");
+  logger.warning("ignored token");
   return false;
 }
 
@@ -387,7 +390,7 @@ TPushParser::do_subscript()
     }
   else
     {
-      logger.warning("token ignored");
+      logger.warning("ignored token");
       return false;
     }
 }
@@ -421,7 +424,7 @@ TPushParser::do_superscript()
     {
       if (parent["over"] == "1")
         {
-         logger.warning("token ignored: already over");
+         logger.warning("already over");
          return false;
        }
       else
@@ -432,15 +435,24 @@ TPushParser::do_superscript()
     }
   else
     {
-      logger.warning("token ignored");
+      logger.warning("ignored token");
       return false;
     }
 }
 
+bool
+TPushParser::do_ignorablespace(const std::string& s)
+{
+  // At the moment, do nothing
+}
+
 bool
 TPushParser::do_space(const std::string&)
 {
-  return false;
+  TNode elem = doc.createS(nextId++);
+  cursor.replace(elem);
+  advance(elem);
+  return true;
 }
 
 bool
@@ -502,13 +514,13 @@ TPushParser::do_apostrophe()
       else
        {
          // is it an error?
-         logger.warning("parser: you have to type an identifier before  ''");
+         logger.warning("you have to insert an identifier before a  ''");
          return false;
        }
     }
   else
     {
-      logger.warning("token ignored: you have to be in a group");
+      logger.warning("cursor has to be in a group");
       return false;
     }
 }
@@ -536,7 +548,7 @@ bool
 TPushParser::do_active(const std::string&)
 {
   // ??? space?
-  logger.warning("token ignorde");
+  logger.warning("ignored token");
   return false;
 }
 
@@ -572,7 +584,7 @@ TPushParser::do_cr()
   else
     {
       // at the moment, \cr can only be used inside a table
-      logger.warning("token ignored: cr used outside a table");
+      logger.warning("cr used outside a table");
       return false;
     }
 }
@@ -681,14 +693,14 @@ TPushParser::do_control(const std::string& name)
            else
              {
                // a macro with arguments or a rightOpen or leftOpen macro must be a group's child
-               logger.warning("token ignored: this macro should be in a group");
+               logger.warning("ignored token: this macro should be in a group");
                return false;
              }
          }
          break;
        case TDictionary::UNDEFINED:
          {
-           logger.warning("parser: using undefined macro " + name);
+           logger.warning("using undefined macro " + name);
            TNode m = doc.createC(name, nextId++);
            cursor.replace(m);
            advance(m);
@@ -698,7 +710,7 @@ TPushParser::do_control(const std::string& name)
        default:
          {
            //assert(0);
-           logger.warning("token ignored");
+           logger.warning("ignored token");
            return false;
          }
        }
@@ -711,7 +723,7 @@ TPushParser::drop_prev_token(bool special)
   assert(cursor.prev());
   assert(cursor.parent());
   TNode prev = cursor.prev();
-  assert(prev.is("i") || prev.is("o") || prev.is("n"));
+  assert(prev.isT());
  
   DOM::UCS4String ucs4val = prev.element().getAttribute("val");
   bool macro = prev.element().hasAttribute("name");
@@ -731,7 +743,7 @@ TPushParser::drop_prev_token(bool special)
       frame.pos--;
     }
 
-  if ((ucs4val.length() > 1) && !special)
+  if ((ucs4val.length() > 1))
     {
       if (!macro)
         {
@@ -739,18 +751,23 @@ TPushParser::drop_prev_token(bool special)
          // to convert it in a utf8
          DOM::GdomeString gdsval(ucs4val);
          std::string utf8val(gdsval);
-         utf8val = utf8val.erase(utf8val.length() - 1, 1);
-         return std::string(utf8val);
+         switch (utf8val[utf8val.length() - 1])
+           {
+           case '-':
+           case '_':
+             return (special) ? std::string(utf8val, 0, utf8val.length() - 1) + "\\" : std::string(utf8val, 0, utf8val.length() - 1);
+           default: return (special) ? "" : std::string(utf8val, 0, utf8val.length() - 1);
+           }
        }
       else
         {
          // in this case, the content of val could be in unicode, 
-         // but we have attribute name, which doesn't contain character not representable 
+         // but we have the attribute name, which doesn't contain character not representable 
          // with a byte.
-         return "\\" + utf8name.erase(utf8name.length() - 1, 1);
+         return (special) ? "\\" + utf8name : "";
        }
     }
-  else if ((ucs4val.length() <= 1) && macro && special) return "\\" + utf8name.erase(utf8name.length() - 1, 1);
+  else if (macro && special) return "\\" + utf8name;
   else return "";
 }
 
@@ -769,9 +786,9 @@ TPushParser::drop_prev_script(bool special)
   // child has been removed yet.
   if (cursor.prev().isG() && !prev.hasId())
     {
-      // in this case, the user has inserted the a sequence of '.
-      // Hence, we force a normal deleting, because the behaviour must be the same 
-      // for the two kind of deleting
+      // in this case, the user has inserted a sequence of '.
+      // Hence, we force a normal deletion, because the behavior must be the same 
+      // for the two kind of deletion
       return drop_prev(false);
     }
   else return drop_prev(special);
@@ -788,6 +805,8 @@ TPushParser::drop_prev_group(bool special)
 
   if (parent.isC() && prev.hasId())
     {
+      // this previous group is a macro's argument. Entering inside it means that
+      // this argument becomes incomplete. Hence, we have to decrement the member pos.
       assert(!frames.empty());
       frames.top().pos--;
     }
@@ -817,9 +836,8 @@ TPushParser::drop_prev_macro(bool special)
   
   if (!entry.defined())
     {
-      // We can assume that the user wants to completely delete the undefined macro, 
-      // but we can also handle this case as we handle tokens. At the moment, we delete the 
-      // whole macro
+      // In this case, with a normal deletion, we completely remove the macro.
+      // With a special deletion, we remove the last character of the macro's name.
       cursor.remove();
       prev.replace(cursor);
       if (cursor.parent().isC())
@@ -828,7 +846,7 @@ TPushParser::drop_prev_macro(bool special)
          assert(!frames.empty());
          frames.top().pos--;
        }
-      if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+      if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1); // we remove the last char, because an undefined macro's name is visible
       return "";
     }
   else
@@ -842,7 +860,7 @@ TPushParser::drop_prev_macro(bool special)
       if (entry.rightOpen)
         {
          // In this fragment of code we also handle the leftOpen && rightOpen MACRO.
-         // if the control element is rightOpen, the cursor should be placed after 
+         // since the control element is rightOpen, the cursor should be placed after 
          // the last child of the control element's last child, and than, we try to remove something.
          // A frame MUST be pushed in the stack, because we dont' know if the following actions 
          // will completely remove the MACRO.
@@ -867,8 +885,9 @@ TPushParser::drop_prev_macro(bool special)
          // In this case, we do not have to push a frame in the stack, because we remove the 
          // MACRO immediately, substituting it with the content of the phantom group.
          // We could remove the last child of the phantom group, but
-         // it's not clear if it's the correct behavior of the graphical deleting.
-         // At the moment, to give a standard behaviour, we remove the last element.
+         // it's not clear if it's the correct behavior of the graphical deletion.
+         // At the moment, to give a standard behavior, we remove the last element.
+         // With a special deletion, we do not remove it.
          assert(prev.first());
          assert(prev.first().isG());
          assert(prev.first() == prev.last());
@@ -881,7 +900,7 @@ TPushParser::drop_prev_macro(bool special)
              g.remove();
              prev.replace(g.first(), TNode());
              parent.append(cursor);
-             if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+             if (special) return "\\" + macro_name;
              else return do_drop(special);
            }
          else
@@ -890,7 +909,7 @@ TPushParser::drop_prev_macro(bool special)
              cursor.remove();
              g.remove();
              prev.replace(cursor);
-             if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+             if (special) return "\\" + macro_name;
              else
                {
                  // Once removed this empty macro, we could try to remove something else.
@@ -921,7 +940,7 @@ TPushParser::drop_prev_macro(bool special)
 
                  std::string last_del = entry.pattern[entry.pattern.size() - 1].value;
 
-                 return "\\" + last_del.erase(last_del.length() - 1, 1);
+                 return "\\" + last_del;
                }
              else
                {
@@ -937,7 +956,7 @@ TPushParser::drop_prev_macro(bool special)
                  // now, p is the correct value of pos, and we can push the frame.
                  frames.push(Frame(entry, p));
                  
-                 // To give a standard behaviour to the graphical deleting, we remove the last 
+                 // To give a standard behavior to the graphical deletion, we remove the last 
                  // element of the macro. Since we are in a phantom group, we can invoke the 
                  // do_drop_phantom_group(special).
                  return do_drop_phantom_group(special);
@@ -965,7 +984,7 @@ TPushParser::drop_prev_macro(bool special)
                    {
                      // to type a table with rows and cells, the user had typed a 
                      // "{", and to exit from it, the user had inserted a "}".
-                     // Since we are in a special deleting, we just idealy remove the "}"
+                     // Since we are in a special deletion, we just idealy remove the "}"
                      return "";
                    }
                  else return do_drop_phantom_group(special);
@@ -999,12 +1018,12 @@ TPushParser::drop_prev_macro(bool special)
              frames.top().pos--;
            }
 
-         if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+         if (special) return "\\" + macro_name;
          else return "";
                  
-         // now we could start to remove something else. This behaviour would be justified by the 
+         // now we could start to remove something else. This behavior would be justified by the 
          // fact that, generally, an empty MACRO gives no visual information about it.
-         // To adopt this behaviour, just remove the comment to the following instruction
+         // To adopt this behavior, just remove the comment to the following instruction
          // return do_drop(special);
        }
     } // end of defined MACRO
@@ -1014,14 +1033,14 @@ TPushParser::drop_prev_macro(bool special)
 std::string
 TPushParser::drop_prev(bool special)
 {
-  // if in this function, the prev of cursor does exist, also the parent and we want a graphical deleting.
+  // if in this function, the prev of cursor does exist, also the parent and we want a graphical deletion.
   
   assert(cursor.prev());
   assert(cursor.parent());
 
   TNode prev = cursor.prev();
 
-  if (prev.is("i") || prev.is("o") || prev.is("n"))
+  if (prev.isT())
     {
       return drop_prev_token(special);
     }
@@ -1120,15 +1139,6 @@ TPushParser::do_drop_script(bool special)
          // Since we don't know who is cursor's parent, and who is cursor's preceding 
          // element, we invoke the do_drop()
          return do_drop(special);
-         
-         /*
-          * * the following istructions have sense, only if we remove the preceding one.
-          * 
-         // if the new parent is a group with Id and the cursor is the only 
-         // element of this group, we have to remove the group. These controls are made
-         // in the method rgreplace_father().
-         if (cursor.parent().isG() && cursor.parent().hasId()) rgreplace_father();
-         */
        }
     }
   else
@@ -1142,7 +1152,7 @@ TPushParser::do_drop_script(bool special)
       if (special) return "";
       else
         {
-         // to give a standard behaviour, we try to remove the element, which was 
+         // to give a standard behavior, we try to remove the element, which was 
          // the script's base.
          return do_drop(special);
        }
@@ -1161,7 +1171,7 @@ TPushParser::do_drop_macro(bool special)
   assert(cursor.parent() && cursor.parent().isC());
   TNode parent = cursor.parent();
 
-  // this string is useful iff we have a special deleting
+  // this string is useful iff we have a special deletion.
   std::string macro_name = parent.nameC();
   
   assert(!frames.empty());
@@ -1180,31 +1190,12 @@ TPushParser::do_drop_macro(bool special)
       parent.replace(cursor);
       frames.pop();
 
-      if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+      if (special) return "\\" + macro_name;
       else
         {
-         // Since the macro hadn't no children and this is a graphical deleting, we try 
+         // Since the macro had no children and this is a graphical deletion, we try 
          // to remove something else
          return do_drop(special);
-
-          /*
-           * the following block of code has sense only if we remove the preceding instruction
-           * 
-           // if the new parent is a group with Id, and has no elements other than the 
-           // cursor, we can remove it, because it' a graphical deleting
-           if (cursor.parent() && cursor.parent().isG() && cursor.parent().hasId())
-            rgreplace_father();
-           else if (cursor.parent().isC())
-             {
-              // We have assumed that a MACRO cannot be a MACRO's child. 
-              // At the moment, this assumption is valid, but in a future 
-              // it might be false.
-              assert(!frames.empty());
-              Frame& frame = frames.top();
-              assert(frame.pos > 0);
-              frame.pos--;
-            }
-          */
        }
     }
   else
@@ -1228,7 +1219,7 @@ TPushParser::do_drop_macro(bool special)
              // two units: the delimiter and the actual argument
              std::string last_del = frame.entry.pattern[frame.pos - 1].value;
              frame.pos = frame.pos - 2;
-             return "\\" + last_del.erase(last_del.length() - 1, 1);
+             return "\\" + last_del;
            }
          else
            {
@@ -1237,7 +1228,7 @@ TPushParser::do_drop_macro(bool special)
              assert(sequence_length);
              frame.pos = frame.pos - sequence_length - 1;
              
-             // since it's a graphical deleting, we have to remove the current preceding element.
+             // since it's a graphical deletion, we have to remove the current preceding element.
              // We don't invoke the drop_prev(), because a do_drop_phantom_group is more general.
              return do_drop_phantom_group(special);
            }
@@ -1246,7 +1237,7 @@ TPushParser::do_drop_macro(bool special)
         {
          // the prev is not a delimited argument, so we have to try to remove it. 
          // We "try", because the prev might be something that 
-         // a simple delete cannot remove completely
+         // a simple deletion cannot remove completely
          return drop_prev(special);
        }
     }
@@ -1294,7 +1285,7 @@ TPushParser::do_drop_groupId(bool special)
       else
         {
          rgreplace_father();
-         // we have to re-start the process, because it' a graphical deleting
+         // we have to re-start the process, because it' a graphical deletion
          return do_drop(special);
        }
     }
@@ -1331,7 +1322,7 @@ TPushParser::do_drop_phantom_group(bool special)
                    {
                      std::string del = frame.entry.pattern[frame.pos].value;
                      frame.pos--;
-                     return "\\" + del.erase(del.length() - 1, 1);
+                     return "\\" + del;
                    }
                }
              else
@@ -1404,7 +1395,7 @@ TPushParser::do_drop_phantom_group(bool special)
          assert(!frames.empty());
           Frame& frame = frames.top();
 
-         // this variable is useful in a special deleting
+         // this variable is useful in a special deletion
          std::string macro_name = gfather.nameC();
          
          if (frame.entry.leftOpen && frame.entry.rightOpen)
@@ -1437,10 +1428,10 @@ TPushParser::do_drop_phantom_group(bool special)
              // this MACRO no longer exists.
              frames.pop();
 
-             if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+             if (special) return "\\" + macro_name;
              else
                {
-                 // to give a standard behaviour to the graphical deleting, we call the do_drop.
+                 // to give a standard behavior to the graphical deletion, we call the do_drop.
                  return do_drop(special);
                }
            }
@@ -1458,10 +1449,10 @@ TPushParser::do_drop_phantom_group(bool special)
              // now we have the situation preceding the rightOpen MACRO, so we have to pop the frame
              frames.pop();
 
-             if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+             if (special) return "\\" + macro_name;
              else
                {
-                 // to give a standard behaviour to the graphical deleting, we call the do_drop.
+                 // to give a standard behavior to the graphical deletion, we call the do_drop.
                  return do_drop(special);
                }
              
@@ -1490,7 +1481,7 @@ TPushParser::do_drop_phantom_group(bool special)
                  gfather.replace(cursor);
                  frames.pop();
 
-                 if (special) return "\\" + macro_name.erase(macro_name.length() - 1, 1);
+                 if (special) return "\\" + macro_name;
                  else
                    {
                      // once we have replaced the empty macro with the cursor, we can remove
@@ -1514,7 +1505,7 @@ TPushParser::do_drop_phantom_group(bool special)
                          // argument.
                          std::string last_del = frame.entry.pattern[frame.pos - 1].value;
                          frame.pos = frame.pos - 2;
-                         return "\\" +  last_del.erase(last_del.length() - 1, 1)
+                         return "\\" +  last_del; 
                        }
                      else
                        {
@@ -1564,7 +1555,7 @@ TPushParser::do_drop_phantom_group(bool special)
          // a cell MUST be a row's child, which in turn is a table's child 
          assert(gfather.parent() && gfather.parent().is("row") && gfather.parent().parent());
 
-         // this variable is useful to handle the special deleting
+         // this variable is useful to handle the special deletion
          std::string table_name = gfather.parent().parent().nameC();
          
          TNode row = gfather.parent();
@@ -1616,8 +1607,8 @@ TPushParser::do_drop_phantom_group(bool special)
                  assert(last_cell.first().isG() && !last_cell.first().hasId());
                  last_cell.first().append(cursor);
                  // Since cells and rows are separated by spaces and CRs 
-                 // (and the user can see this spaces and CRs), a special deleting 
-                 // is equivalent to a normal deleting
+                 // (and the user can see this spaces and CRs), a special deletion 
+                 // is equivalent to a normal deletion
                  return "";
                }
            } // end of if (!prev_cell)
@@ -1649,13 +1640,13 @@ TPushParser::do_drop_phantom_group(bool special)
         {
          // in this case we ignore the user's will of deleting
          // but we could also decide to remove the math mode.
-         logger.warning("Parser: nothing to delete");
+         logger.warning("nothing to delete");
          return "";
        }
       else
         {
          // cursor's grand father is undefined
-         logger.error("parser: TML tree is in a unknown state");
+         logger.error("TML tree is in an unknown state");
          return "";
        }
     } // end of the else of the if (prev)
@@ -1714,21 +1705,22 @@ TPushParser::process(const TToken& token)
 {
   switch (token.category)
     {
-    case TToken::BEGIN: return do_begin(); break;
-    case TToken::END: return do_end(); break;
-    case TToken::SHIFT: return do_shift(); break;
-    case TToken::ALIGN: return do_align(); break;
-    case TToken::EOL: return do_eol(); break;
-    case TToken::PARAMETER: return do_parameter(token.value); break;
-    case TToken::SUPERSCRIPT: return do_superscript(); break;
-    case TToken::SUBSCRIPT: return do_subscript(); break;
-    case TToken::SPACE: return do_space(token.value); break;
-    case TToken::LETTER: return do_letter(token.value); break;
-    case TToken::DIGIT: return do_digit(token.value); break;
-    case TToken::OTHER: return do_other(token.value); break;
-    case TToken::ACTIVE: return do_active(token.value); break;
-    case TToken::COMMENT: return do_comment(); break;
-    case TToken::CONTROL: return do_control(token.value); break;
+    case TToken::BEGIN: return do_begin();
+    case TToken::END: return do_end();
+    case TToken::SHIFT: return do_shift();
+    case TToken::ALIGN: return do_align();
+    case TToken::EOL: return do_eol();
+    case TToken::PARAMETER: return do_parameter(token.value);
+    case TToken::SUPERSCRIPT: return do_superscript();
+    case TToken::SUBSCRIPT: return do_subscript();
+    case TToken::IGNORABLE_SPACE: return do_ignorablespace(token.value);
+    case TToken::SPACE: return do_space(token.value);
+    case TToken::LETTER: return do_letter(token.value);
+    case TToken::DIGIT: return do_digit(token.value);
+    case TToken::OTHER: return do_other(token.value);
+    case TToken::ACTIVE: return do_active(token.value);
+    case TToken::COMMENT: return do_comment();
+    case TToken::CONTROL: return do_control(token.value);
     }
 }
 
@@ -1782,7 +1774,7 @@ TPushParser::push(const TToken& token)
                    //   - ignore the token, and wait for the correct delimiter
                    //   - ignore the token, wait for the correct delimiter and emit an error
                    // At the moment, we implement the second possibily
-                   logger.warning("parser: it's not the correct delimiter...you have to type " + frame.entry.pattern[frame.pos + 1].value);
+                   logger.warning("it's not the correct delimiter...you have to type '" + frame.entry.pattern[frame.pos + 1].value + "'");
                  }
                else
                  {
@@ -1813,7 +1805,7 @@ TPushParser::push(const TToken& token)
          {
            // As by the TeX parsing rules of undelimited parameters,
            // empty spaces are ignored
-           if (token.category != TToken::SPACE) process(token);
+           if ((token.category != TToken::SPACE) && (token.category != TToken::IGNORABLE_SPACE)) process(token);
          }
        else if (frame.entry.pattern[frame.pos] == token)
          {
@@ -1837,7 +1829,7 @@ TPushParser::push(const TToken& token)
        else
          {
            // There is a mismatch. Emit an error and ignore the token?
-           logger.warning("parser: token ignored: " + token.value);
+           logger.warning("ignored token: " + token.value);
          }
       }
     else