void
    push(int level)
    {
      currentLevel = level;
      if (currentLevel == -1) {