public String toString() {
      StringBuffer m = new StringBuffer();
      m.append("#");
      m.append(sym);
      if (value != null) {
          m.append(" (");
          m.append(value.toString());
          m.append(")");
      }
      if (left >= 0) {
    	  m.append(" @");
          m.append(left);
          if (right >= 0) {
        	  m.append(".");
              m.append(right);
          }
      }
	  return m.toString();
  }