protected void consume(int cc) throws CompilationException {
    if ((cc<0) || (c!=cc)) {
      CompilationException exc=
        new CompilationException(c==-1?1:3,new Character((char)c));
      exc.col=column;
      if (c==-1) exc.col--;
      throw exc;
    };
    read();
  };