116 |
public |
public |
117 |
LineNumberReader(Reader in, int size) |
LineNumberReader(Reader in, int size) |
118 |
{ |
{ |
119 |
super(new PushbackReader(in), size); |
super(in, size); |
120 |
} |
} |
121 |
|
|
122 |
/*************************************************************************/ |
/*************************************************************************/ |
241 |
int extra_char_read = super.read(); |
int extra_char_read = super.read(); |
242 |
|
|
243 |
if ((extra_char_read != '\n') && (extra_char_read != -1)) |
if ((extra_char_read != '\n') && (extra_char_read != -1)) |
244 |
((PushbackReader)in).unread(extra_char_read); |
pos--; |
245 |
|
|
246 |
char_read = '\n'; |
char_read = '\n'; |
247 |
++line_number; |
++line_number; |