]> 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 433b3fdec3b3568f38f453eba1edd11f82622168..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,7 +435,7 @@ TPushParser::do_superscript()
     }
   else
     {
-      logger.warning("token ignored");
+      logger.warning("ignored token");
       return false;
     }
 }
@@ -511,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;
     }
 }
@@ -545,7 +548,7 @@ bool
 TPushParser::do_active(const std::string&)
 {
   // ??? space?
-  logger.warning("token ignorde");
+  logger.warning("ignored token");
   return false;
 }
 
@@ -581,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;
     }
 }
@@ -690,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);
@@ -707,7 +710,7 @@ TPushParser::do_control(const std::string& name)
        default:
          {
            //assert(0);
-           logger.warning("token ignored");
+           logger.warning("ignored token");
            return false;
          }
        }
@@ -783,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 behavior 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);
@@ -882,7 +885,7 @@ 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.
+         // 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());
@@ -953,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 behavior 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);
@@ -981,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);
@@ -1030,7 +1033,7 @@ 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());
@@ -1168,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());
@@ -1190,7 +1193,7 @@ TPushParser::do_drop_macro(bool special)
       if (special) return "\\" + macro_name;
       else
         {
-         // Since the macro had 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);
        }
@@ -1225,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);
            }
@@ -1234,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);
        }
     }
@@ -1282,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);
        }
     }
@@ -1392,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)
@@ -1428,7 +1431,7 @@ TPushParser::do_drop_phantom_group(bool special)
              if (special) return "\\" + macro_name;
              else
                {
-                 // to give a standard behavior 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);
                }
            }
@@ -1449,7 +1452,7 @@ TPushParser::do_drop_phantom_group(bool special)
              if (special) return "\\" + macro_name;
              else
                {
-                 // to give a standard behavior 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);
                }
              
@@ -1552,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();
@@ -1604,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)
@@ -1637,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)
@@ -1771,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
                  {
@@ -1826,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