void write(int b) {
    try {
      text[tsize++]=(byte)b;
    } catch (ArrayIndexOutOfBoundsException exc) {
      byte[] new_text=new byte[text.length<<1];
      System.arraycopy(text, 0, new_text, 0, tsize-1);
      text=new_text;
      text[tsize-1]=(byte)b;
    };
  };