X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FDEVEL%2Fmathml_editor%2Fsrc%2FTPushParser.cc;h=0c96fe43968c94be52a1fdcffac385012d683ebb;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=433b3fdec3b3568f38f453eba1edd11f82622168;hpb=98e5817ce4fa424fb3181d90d327935c1b100ec4;p=helm.git

diff --git a/helm/DEVEL/mathml_editor/src/TPushParser.cc b/helm/DEVEL/mathml_editor/src/TPushParser.cc
index 433b3fdec..0c96fe439 100644
--- a/helm/DEVEL/mathml_editor/src/TPushParser.cc
+++ b/helm/DEVEL/mathml_editor/src/TPushParser.cc
@@ -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