4 public class LineReader {
6 private static int MAXBUF = 1024 * 16;
7 char[] buf = new char[MAXBUF];
10 Vec pushback = new Vec();
12 public LineReader(Reader r) { this.r = r; }
14 public void pushback(String s) { pushback.push(s); }
16 public String readLine() throws IOException {
18 if (pushback.size() > 0) return (String)pushback.pop();
19 for(int i=0; i<buflen; i++) {
22 if (buf[i-1] == '\r') ret = new String(buf, 0, i-1);
23 else ret = new String(buf, 0, i);
24 System.arraycopy(buf, i+1, buf, 0, buflen - (i+1));
29 int numread = r.read(buf, buflen, MAXBUF - buflen);
31 if (buflen == 0) return null;
32 String ret = new String(buf, 0, buflen);