/******************************************************************************
BufferedInput extends the BufferedInputStream by providing character and line
counting plus a few additional methods providing low level scanning operations.

Obsolete design -- based on FlexOr written in C where we exported entities such
as nextChar and currentChar.  In OO and using the BufferedInputStream it is a
poor design.  The user of BufferedInput would keep a local copy of current char.
In addition, BufferedInputStream provides, through mark and reset, a more
general method of look ahead than provided in FlexOr.  We should make use of
that, however, it turns out we cannot do so for simple scanning of logical
characters consisting of pairs, or more, of physical characters as the two
look aheads interfere.  For example, \r\n for end of line in MSDOS and </ in
HTML.

----------------------------------------------------
Copyright (c) Gunnar Gotshalks. All Rights Reserved.

Permission to use, copy, modify, and distribute this software
and its documentation for NON-COMMERCIAL purposes and
without fee is hereby granted. 
******************************************************************************/

package FlexOr.io;
import java.io.*;

/**
BufferedInput extends the BufferedInputStream by providing the features for
simple scanning of input.

<P>The Java file input API read method always returns a character, including
an unbounded number of EOF characters when the end of file is reached.
Consequently, all input files are implicitly unbounded in length giving the
following structure for a file.
<PRE>  file = input[0..N-1 , N, ...] </PRE>
where a file contains the  <tt>N</TT> data characters <TT>input[0..N-1] and
EOF characters in <TT>input[N, N+1, ...]</TT>.


<P>The EOL character (end-ofline) always counts as one data character.  See the
method <TT>read</TT>

<P><B>Class invariant:</B> 
  <TT>currentChar = input[i] => nextChar = input[i+1];</TT>
<P>
@author Gunnar Gotshalks
@version 1.0 1999 Jan 10
*/

public class BufferedInput extends BufferedInputStream {

/******************************************************************************
Creating an instance of BufferedInput opens the file named by the String.
There is no open required by the user. In the OO paradigm opening a file
is analogous to creating a new object unlike procedural paradigm where
the same variables are reused for each file.

<P><PRE><B>Requires:</B> True
<B>Ensures:</B> currentChar = input[0]  // first char in the file
</PRE>
@exception FileNotFoundException when the file named by fileName cannot be
opened.
*/

public BufferedInput (String fileName) throws FileNotFoundException {
  super(new FileInputStream(fileName));
  try {
    nextChar = super.read();     // prime the pump.
  } catch (IOException e) { System.err.println("Trouble reading" + e); }
}

/******************************************************************************
Processing a text file usually requires a scanner which needs to: (1) examine
the current input character more than once; and (2) often needs to look ahead
one character.  To help programmers we provide currentChar to hold the
last character input by the program and nextChar to hold the next character to
be read by the program.
*/

protected int currentChar = Char.EOF;
protected int nextChar = Char.EOF;

/**
The current character is the one to process next from the input file.
<P><PRE><B>Requires:</B> user called read i times
<B>Ensures:</B> result = currentChar
     and currentChar = input[i-1]
</PRE>
*/
public int getCurrentChar() { return currentChar; }

/**
The next character is a look ahead character.
<P><PRE><B>Requires:</B> user called read i times
<B>Ensures:</B> result = nextChar
    and nextChar = input[i]
</PRE>
*/
public int getNextChar() { return nextChar; }

/******************************************************************************
To help programmers provide input statistics in application programs we
provide charCount to count the total number of characters input from a file,
and lineCount to count the input lines.
---------------------------*/

protected int charCount = 0 , lineCount = 0;

/**
Return the number of data characters read from the file.
<P><PRE><B>Requires:</B> True
<B>Ensures:</B>i : 0..N-1 | currentChar = input[i] => result = i+1
          and i: N, ... | currentChar = input[i] => result = N
</PRE>
*/
public int getCharCount() { return charCount; }

public int getLineCount() { return lineCount; }

/******************************************************************************
Requires: True
Ensures: currentChar = old nextChar
         nextChar = next character from the file or EOF if at
   the end of file.

No need to test for EOF before reading as Java returns EOF an unbounded number
of times.

Need to have different cases depending upon how end-of-line is represented.
On Macintosh it is '\r' (13), on Unix is is '\n' (10), on Windows it is
'\r\n'.  This means that after recognizing '\r' we must skip a following '\n'.
End-of-line always counts as 1 character.  EOF does not count as a character.
---------------------------*/

public int read() {
  currentChar = nextChar;
  try {
    nextChar = super.read();
    charCount++;
    switch (currentChar) {
      case 13 : lineCount++ ; currentChar = Char.EOL;
                if (nextChar == 10) nextChar = super.read(); break;
      case 10 : lineCount++ ; currentChar = Char.EOL; break;
      case -1 : currentChar = Char.EOF; charCount--; break;
    }
  } catch (IOException e) { System.err.println("Trouble reading" + e); }

  return currentChar;
}

/******************************************************************************
Requires: currentChar be the first character of the line to read.
Ensures: result string contains the characters in the line up to the
  end-of-line.  currentChar is the first character on the next line.
---------------------------*/

public String readLine() {
  StringBuffer buffer = new StringBuffer(100);
  while ((currentChar != Char.EOF) && (currentChar != Char.EOL)) {
    buffer.append((char) currentChar);
    read();
  }
  read();   // Advance to first character on the next line.
  return buffer.toString();
}

/*****************************************************************************
Requires: True
Ensures: old currentChar .. currentChar-1 are white space.
         currentChar is not a white space character (could be EOF)
---------------------------*/

public void skipWhitespaces() {
  while (Character.isWhitespace((char) currentChar)) read();  
}

/*****************************************************************************
Requires: True
Ensures: forall c : old currentChar .. currentChar-2 | c ~= EOL and c ~= EOF
         currentChar-1 = EOL =>
             currentChar = first character on the next line or EOF
         currentChar-1 = EOF => currentChar = EOF
---------------------------*/

public void skipToNextLine() {
  while((currentChar != Char.EOL) && (currentChar != Char.EOF)) read();
  if (currentChar == Char.EOL) read();  // get to first char on next line
}

}