DataInput and DataOutput interfaces to allow
 * the reading and writing of Java primitives.
 *
 * @author Aaron M. Renn RandomAccessFile
   * to read from the specified File object with the specified 
   * access mode.   The access mode is either "r" for read only access or "rw" 
   * for read-write access.
   * 
   * Note that a SecurityManager check is made prior to
   * opening the file to determine whether or not this file is allowed to
   * be read or written.
   *
   * @param file The File object to read and/or write.
   * @param mode "r" for read only or "rw" for read-write access to the file
   *
   * @exception IllegalArgumentException If mode has an 
   * illegal value
   * @exception SecurityException If the requested access to the file 
   * is not allowed
   * @exception IOException If any other error occurs
   */
  public RandomAccessFile (File file, String mode)
    throws FileNotFoundException
  {
    this (file.getPath(), mode);
  }
  /**
   * This method initializes a new instance of RandomAccessFile
   * to read from the specified file name with the specified access mode.
   * The access mode is either "r" for read only access, "rw" for read
   * write access, "rws" for synchronized read/write access of both
   * content and metadata, or "rwd" for read/write access
   * where only content is required to be synchronous.
   * 
   * Note that a SecurityManager check is made prior to
   * opening the file to determine whether or not this file is allowed to
   * be read or written.
   *
   * @param fileName The name of the file to read and/or write
   * @param mode "r", "rw", "rws", or "rwd"
   *
   * @exception IllegalArgumentException If mode has an 
   * illegal value
   * @exception SecurityException If the requested access to the file 
   * is not allowed
   * @exception FileNotFoundException If any other error occurs
   */
  public RandomAccessFile (String fileName, String mode)
    throws FileNotFoundException
  {
    int fdmode;
    if (mode.equals("r"))
      fdmode = FileChannelImpl.READ;
    else if (mode.equals("rw"))
      fdmode = FileChannelImpl.READ | FileChannelImpl.WRITE;
    else if (mode.equals("rws"))
      {
	fdmode = (FileChannelImpl.READ | FileChannelImpl.WRITE
		  | FileChannelImpl.SYNC);
      }
    else if (mode.equals("rwd"))
      {
	fdmode = (FileChannelImpl.READ | FileChannelImpl.WRITE
		  | FileChannelImpl.DSYNC);
      }
    else
      throw new IllegalArgumentException ("invalid mode: " + mode);
    // The obligatory SecurityManager stuff
    SecurityManager s = System.getSecurityManager();
    if (s != null)
      {
        s.checkRead(fileName);
        if ((fdmode & FileChannelImpl.WRITE) != 0)
          s.checkWrite(fileName);
      }
    ch = new FileChannelImpl (fileName, fdmode);
    fd = new FileDescriptor(ch);
    out = new DataOutputStream (new FileOutputStream (fd));
    in = new DataInputStream (new FileInputStream (fd));
  }
  /**
   * This method closes the file and frees up all file related system
   * resources.  Since most operating systems put a limit on how many files
   * may be opened at any given time, it is a good idea to close all files
   * when no longer needed to avoid hitting this limit
   */
  public void close () throws IOException
  {
    ch.close();
  }
  /**
   * This method returns a FileDescriptor object that 
   * represents the native file handle for this file.
   *
   * @return The FileDescriptor object for this file
   *
   * @exception IOException If an error occurs
   */
  public final FileDescriptor getFD () throws IOException
  {
    synchronized (this)
      {
	if (fd == null)
	  fd = new FileDescriptor (ch);
	return fd;
      }
  }
  /**
   * This method returns the current offset in the file at which the next
   * read or write will occur
   *
   * @return The current file position
   *
   * @exception IOException If an error occurs
   */
  public long getFilePointer () throws IOException
  {
    return ch.position();
  }
  /**
   * This method sets the length of the file to the specified length.  If
   * the currently length of the file is longer than the specified length,
   * then the file is truncated to the specified length.  If the current
   * length of the file is shorter than the specified length, the file
   * is extended with bytes of an undefined value.
   *  
   * The file must be open for write access for this operation to succeed.
   *
   * @param newlen The new length of the file
   *
   * @exception IOException If an error occurs
   */
  public void setLength (long newLen) throws IOException
  {
    ch.truncate (newLen);
  }
  /**
   * This method returns the length of the file in bytes
   *
   * @return The length of the file
   *
   * @exception IOException If an error occurs
   */
  public long length () throws IOException
  {
    return ch.size();
  }
  /**
   * This method reads a single byte of data from the file and returns it
   * as an integer.
   *
   * @return The byte read as an int, or -1 if the end of the file was reached.
   *
   * @exception IOException If an error occurs
   */
  public int read () throws IOException
  {
    return in.read();
  }
  /**
   * This method reads bytes from the file into the specified array.  The
   * bytes are stored starting at the beginning of the array and up to 
   * buf.length bytes can be read.
   *
   * @param buf The buffer to read bytes from the file into
   *
   * @return The actual number of bytes read or -1 if end of file
   *
   * @exception IOException If an error occurs
   */
  public int read (byte[] buffer) throws IOException
  {
    return in.read (buffer);
  }
  /**
   * This methods reads up to len bytes from the file into the
   * specified array starting at position offset into the array.
   *
   * @param buf The array to read the bytes into
   * @param offset The index into the array to start storing bytes
   * @param len The requested number of bytes to read
   *
   * @return The actual number of bytes read, or -1 if end of file
   *
   * @exception IOException If an error occurs
   */
  public int read (byte[] buffer, int offset, int len) throws IOException
  {
    return in.read (buffer, offset, len);
  }
  /**
   * This method reads a Java boolean value from an input stream.  It does
   * so by reading a single byte of data.  If that byte is zero, then the
   * value returned is false  If the byte is non-zero, then
   * the value returned is true
   * 
   * This method can read a boolean written by an object 
   * implementing the
   * writeBoolean() method in the DataOutput 
   * interface.
   *
   * @return The boolean value read
   *
   * @exception EOFException If end of file is reached before reading the 
   * boolean
   * @exception IOException If any other error occurs
   */
  public final boolean readBoolean () throws IOException
  {
    return in.readBoolean ();
  }
  /**
   * This method reads a Java byte value from an input stream.  The value
   * is in the range of -128 to 127.
   * 
   * This method can read a byte written by an object 
   * implementing the 
   * writeByte() method in the DataOutput interface.
   *
   * @return The byte value read
   *
   * @exception EOFException If end of file is reached before reading the byte
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final byte readByte () throws IOException
  {
    return in.readByte ();
  }
  /**
   * This method reads a Java char value from an input stream.  
   * It operates by reading two bytes from the stream and converting them to 
   * a single 16-bit Java char  The two bytes are stored most
   * significant byte first (i.e., "big endian") regardless of the native
   * host byte ordering. 
   * 
   * As an example, if byte1 and byte2 represent 
   * the first
   * and second byte read from the stream respectively, they will be
   * transformed to a char in the following manner:
   * 
   * (char)(((byte1 & 0xFF) << 8) | (byte2 & 0xFF)
   * 
   * This method can read a char written by an object 
   * implementing the
   * writeChar() method in the DataOutput interface.
   *
   * @return The char value read 
   *
   * @exception EOFException If end of file is reached before reading the char
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final char readChar () throws IOException
  {
    return in.readChar();
  }
  /**
   * This method reads a Java double value from an input stream.  It operates
   * by first reading a logn value from the stream by calling the
   * readLong() method in this interface, then 
   * converts that long
   * to a double using the longBitsToDouble 
   * method in the class java.lang.Double
   * 
   * This method can read a double written by an object 
   * implementing the
   * writeDouble() method in the DataOutput 
   * interface.
   *
   * @return The double value read
   *
   * @exception EOFException If end of file is reached before reading 
   * the double
   * @exception IOException If any other error occurs
   *
   * @see java.lang.Double
   * @see DataOutput
   */
  public final double readDouble () throws IOException
  {
    return in.readDouble ();
  }
  /**
   * This method reads a Java float value from an input stream.  It operates
   * by first reading an int value from the stream by calling the
   * readInt() method in this interface, then converts 
   * that int
   * to a float using the intBitsToFloat method in 
   * the class java.lang.Float
   * 
   * This method can read a float written by an object 
   * implementing the
   * writeFloat() method in the DataOutput interface.
   *
   * @return The float value read
   *
   * @exception EOFException If end of file is reached before reading the float
   * @exception IOException If any other error occurs
   *
   * @see java.lang.Float
   * @see DataOutput
   */
  public final float readFloat () throws IOException
  {
    return in.readFloat();
  }
  /**
   * This method reads raw bytes into the passed array until the array is
   * full.  Note that this method blocks until the data is available and
   * throws an exception if there is not enough data left in the stream to
   * fill the buffer
   *
   * @param buf The buffer into which to read the data
   *
   * @exception EOFException If end of file is reached before filling the 
   * buffer
   * @exception IOException If any other error occurs
   */
  public final void readFully (byte[] buffer) throws IOException
  {
    in.readFully(buffer);
  }
  /**
   * This method reads raw bytes into the passed array buf 
   * starting
   * offset bytes into the buffer.  The number of bytes read 
   * will be
   * exactly len  Note that this method blocks until the data is 
   * available and throws an exception if there is not enough data left in 
   * the stream to read len bytes.
   *
   * @param buf The buffer into which to read the data
   * @param offset The offset into the buffer to start storing data
   * @param len The number of bytes to read into the buffer
   *
   * @exception EOFException If end of file is reached before filling 
   * the buffer
   * @exception IOException If any other error occurs
   */
  public final void readFully (byte[] buffer, int offset, int count)
    throws IOException
  {
    in.readFully (buffer, offset, count);
  }
  /**
   * This method reads a Java int value from an input stream
   * It operates by reading four bytes from the stream and converting them to 
   * a single Java int  The bytes are stored most
   * significant byte first (i.e., "big endian") regardless of the native
   * host byte ordering. 
   * 
   * As an example, if byte1 through byte4 
   * represent the first
   * four bytes read from the stream, they will be
   * transformed to an int in the following manner:
   * 
   * (int)(((byte1 & 0xFF) << 24) + ((byte2 & 0xFF) << 16) + 
   * ((byte3 & 0xFF) << 8) + (byte4 & 0xFF)))
   * 
* The value returned is in the range of 0 to 65535. *
   * This method can read an int written by an object 
   * implementing the
   * writeInt() method in the DataOutput interface.
   *
   * @return The int value read
   *
   * @exception EOFException If end of file is reached before reading the int
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final int readInt () throws IOException
  {
    return in.readInt();
  }
  /**
   * This method reads the next line of text data from an input stream.
   * It operates by reading bytes and converting those bytes to 
   * char
   * values by treating the byte read as the low eight bits of the 
   * char
   * and using 0 as the high eight bits.  Because of this, it does
   * not support the full 16-bit Unicode character set.
   * 
   * The reading of bytes ends when either the end of file or a line terminator
   * is encountered.  The bytes read are then returned as a String
   * A line terminator is a byte sequence consisting of either 
   * \r \n or \r\n  These 
   * termination charaters are
   * discarded and are not returned as part of the string.
   * 
   * This method can read data that was written by an object implementing the
   * writeLine() method in DataOutput
   *
   * @return The line read as a String
   *
   * @exception IOException If an error occurs
   *
   * @see DataOutput
   */
  public final String readLine () throws IOException
  {
    return in.readLine ();
  }
  /**
   * This method reads a Java long value from an input stream
   * It operates by reading eight bytes from the stream and converting them to 
   * a single Java long  The bytes are stored most
   * significant byte first (i.e., "big endian") regardless of the native
   * host byte ordering. 
   * 
   * As an example, if byte1 through byte8 
   * represent the first
   * eight bytes read from the stream, they will be
   * transformed to an long in the following manner:
   * 
   * 
   * (long)((((long)byte1 & 0xFF) << 56) + (((long)byte2 & 0xFF) << 48) + 
   * (((long)byte3 & 0xFF) << 40) + (((long)byte4 & 0xFF) << 32) + 
   * (((long)byte5 & 0xFF) << 24) + (((long)byte6 & 0xFF) << 16) + 
   * (((long)byte7 & 0xFF) << 8) + ((long)byte9 & 0xFF)))
   * 
* The value returned is in the range of 0 to 65535. *
   * This method can read an long written by an object 
   * implementing the
   * writeLong() method in the DataOutput interface.
   *
   * @return The long value read
   *
   * @exception EOFException If end of file is reached before reading the long
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final long readLong () throws IOException
  {
    return in.readLong();
  }
  /**
   * This method reads a signed 16-bit value into a Java in from the stream.
   * It operates by reading two bytes from the stream and converting them to 
   * a single 16-bit Java short  The two bytes are stored most
   * significant byte first (i.e., "big endian") regardless of the native
   * host byte ordering. 
   * 
   * As an example, if byte1 and byte2 
   * represent the first
   * and second byte read from the stream respectively, they will be
   * transformed to a short in the following manner:
   * 
   * (short)(((byte1 & 0xFF) << 8) | (byte2 & 0xFF)
   * 
* The value returned is in the range of -32768 to 32767. *
   * This method can read a short written by an object 
   * implementing the
   * writeShort() method in the DataOutput interface.
   *
   * @return The short value read
   *
   * @exception EOFException If end of file is reached before reading the value
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final short readShort () throws IOException
  {
    return in.readShort();
  }
  /**
   * This method reads 8 unsigned bits into a Java int value 
   * from the 
   * stream. The value returned is in the range of 0 to 255.
   * 
   * This method can read an unsigned byte written by an object implementing 
   * the writeUnsignedByte() method in the 
   * DataOutput interface.
   *
   * @return The unsigned bytes value read as a Java int
   *
   * @exception EOFException If end of file is reached before reading the value
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final int readUnsignedByte () throws IOException
  {
    return in.readUnsignedByte();
  }
  /**
   * This method reads 16 unsigned bits into a Java int value from the stream.
   * It operates by reading two bytes from the stream and converting them to 
   * a single Java int  The two bytes are stored most
   * significant byte first (i.e., "big endian") regardless of the native
   * host byte ordering. 
   * 
   * As an example, if byte1 and byte2 
   * represent the first
   * and second byte read from the stream respectively, they will be
   * transformed to an int in the following manner:
   * 
   * (int)(((byte1 & 0xFF) << 8) + (byte2 & 0xFF))
   * 
* The value returned is in the range of 0 to 65535. *
   * This method can read an unsigned short written by an object implementing
   * the writeUnsignedShort() method in the 
   * DataOutput interface.
   *
   * @return The unsigned short value read as a Java int
   *
   * @exception EOFException If end of file is reached before reading the value
   * @exception IOException If any other error occurs
   */
  public final int readUnsignedShort () throws IOException
  {
    return in.readUnsignedShort();
  }
  /**
   * This method reads a String from an input stream that 
   * is encoded in
   * a modified UTF-8 format.  This format has a leading two byte sequence
   * that contains the remaining number of bytes to read.  This two byte
   * sequence is read using the readUnsignedShort() method of this
   * interface.
   * 
   * After the number of remaining bytes have been determined, these bytes
   * are read an transformed into char values.  
   * These char values
   * are encoded in the stream using either a one, two, or three byte format.
   * The particular format in use can be determined by examining the first
   * byte read.  
   * 
   * If the first byte has a high order bit of 0 then
   * that character consists on only one byte.  This character value consists
   * of seven bits that are at positions 0 through 6 of the byte.  As an
   * example, if byte1 is the byte read from the stream, it would
   * be converted to a char like so:
   * 
   * (char)byte1
   * 
   * If the first byte has 110 as its high order bits, then the 
   * character consists of two bytes.  The bits that make up the character
   * value are in positions 0 through 4 of the first byte and bit positions
   * 0 through 5 of the second byte.  (The second byte should have 
   * 10 as its high order bits).  These values are in most significant
   * byte first (i.e., "big endian") order.
   * 
   * As an example, if byte1 and byte2 
   * are the first two bytes
   * read respectively, and the high order bits of them match the patterns
   * which indicate a two byte character encoding, then they would be
   * converted to a Java char like so:
   * 
   * (char)(((byte1 & 0x1F) << 6) | (byte2 & 0x3F))
   * 
   * If the first byte has a 1110 as its high order bits, then the
   * character consists of three bytes.  The bits that make up the character
   * value are in positions 0 through 3 of the first byte and bit positions
   * 0 through 5 of the other two bytes.  (The second and third bytes should
   * have 10 as their high order bits).  These values are in most
   * significant byte first (i.e., "big endian") order.
   * 
   * As an example, if byte1 byte2 
   * and byte3 are the
   * three bytes read, and the high order bits of them match the patterns
   * which indicate a three byte character encoding, then they would be
   * converted to a Java char like so:
   * 
   * (char)(((byte1 & 0x0F) << 12) | ((byte2 & 0x3F) << 6) | 
   * (byte3 & 0x3F))
   * 
   * Note that all characters are encoded in the method that requires the
   * fewest number of bytes with the exception of the character with the
   * value of \u0000 which is encoded as two bytes.  This is 
   * a  modification of the UTF standard used to prevent C language style
   * NUL values from appearing in the byte stream.
   * 
   * This method can read data that was written by an object implementing the
   * writeUTF() method in DataOutput
   * 
   * @return The String read
   *
   * @exception EOFException If end of file is reached before reading the 
   * String
   * @exception UTFDataFormatException If the data is not in UTF-8 format
   * @exception IOException If any other error occurs
   *
   * @see DataOutput
   */
  public final String readUTF () throws IOException
  {
    return in.readUTF();
  }
  /**
   * This method sets the current file position to the specified offset 
   * from the beginning of the file.  Note that some operating systems will
   * allow the file pointer to be set past the current end of the file.
   *
   * @param pos The offset from the beginning of the file at which to set 
   * the file pointer
   *
   * @exception IOException If an error occurs
   */
  public void seek (long pos) throws IOException
  {
    ch.position(pos);
  }
  /**
   * This method attempts to skip and discard the specified number of bytes 
   * in the input stream.  It may actually skip fewer bytes than requested. 
   * The actual number of bytes skipped is returned.  This method will not
   * skip any bytes if passed a negative number of bytes to skip.
   *
   * @param numBytes The requested number of bytes to skip.
   *
   * @return The number of bytes actually skipped.
   *
   * @exception IOException If an error occurs.
   */
  public int skipBytes (int numBytes) throws IOException
  {
    if (numBytes < 0)
      throw new IllegalArgumentException ("Can't skip negative bytes: " +
                                          numBytes);
    
    if (numBytes == 0)
      return 0;
    
    long oldPos = ch.position();
    long newPos = oldPos + numBytes;
    long size = ch.size();
    if (newPos > size)
      newPos = size;
    ch.position(newPos);
    return (int) (ch.position() - oldPos);
  }
  /**
   * This method writes a single byte of data to the file. The file must
   * be open for read-write in order for this operation to succeed.
   *
   * @param The byte of data to write, passed as an int.
   *
   * @exception IOException If an error occurs
   */
  public void write (int oneByte) throws IOException
  {
    out.write(oneByte);
  }
  /**
   * This method writes all the bytes in the specified array to the file.
   * The file must be open read-write in order for this operation to succeed.
   *
   * @param buf The array of bytes to write to the file
   */
  public void write (byte[] buffer) throws IOException
  {
    out.write(buffer);
  }
  /**
   * This method writes len bytes to the file from the specified
   * array starting at index offset into the array.
   *
   * @param buf The array of bytes to write to the file
   * @param offset The index into the array to start writing file
   * @param len The number of bytes to write
   *
   * @exception IOException If an error occurs
   */
  public void write (byte[] buffer, int offset, int len) throws IOException
  {
    out.write (buffer, offset, len);
  }
  /**
   * This method writes a Java boolean to the underlying output 
   * stream. For a value of true, 1 is written to the stream.
   * For a value of false, 0 is written.
   *
   * @param b The boolean value to write to the stream
   *
   * @exception IOException If an error occurs
   */
  public final void writeBoolean (boolean val) throws IOException
  {
    out.writeBoolean(val);
  }
  /**
   * This method writes a Java byte value to the underlying
   * output stream.
   *
   * @param b The byte to write to the stream, passed 
   * as an int.
   *
   * @exception IOException If an error occurs
   */
  public final void writeByte (int v) throws IOException
  {
    out.writeByte(v);
  }
  /**
   * This method writes a Java short to the stream, high byte
   * first.  This method requires two bytes to encode the value.
   *
   * @param s The short value to write to the stream, 
   * passed as an int.
   *
   * @exception IOException If an error occurs
   */
  public final void writeShort (int v) throws IOException
  {
    out.writeShort(v);
  }
  /**
   * This method writes a single char value to the stream,
   * high byte first.
   *
   * @param v The char value to write, passed as 
   * an int.
   *
   * @exception IOException If an error occurs
   */
  public final void writeChar (int v) throws IOException
  {
    out.writeChar(v);
  }
  /**
   * This method writes a Java int to the stream, high bytes
   * first.  This method requires four bytes to encode the value.
   *
   * @param v The int value to write to the stream.
   *
   * @exception IOException If an error occurs
   */
  public final void writeInt (int v) throws IOException
  {
    out.writeInt(v);
  }
  /**
   * This method writes a Java long to the stream, high bytes
   * first.  This method requires eight bytes to encode the value.
   *
   * @param v The long value to write to the stream.
   *
   * @exception IOException If an error occurs
   */
  public final void writeLong (long v) throws IOException
  {
    out.writeLong(v);
  }
  /**
   * This method writes a Java float value to the stream.  This
   * value is written by first calling the method 
   * Float.floatToIntBits
   * to retrieve an int representing the floating point number,
   * then writing this int value to the stream exactly the same
   * as the writeInt() method does.
   *
   * @param v The floating point number to write to the stream.
   *
   * @exception IOException If an error occurs
   *
   * @see #writeInt(int)
   */
  public final void writeFloat (float v) throws IOException
  {
    out.writeFloat(v);
  }
  /**
   * This method writes a Java double value to the stream.  This
   * value is written by first calling the method 
   * Double.doubleToLongBits
   * to retrieve an long representing the floating point number,
   * then writing this long value to the stream exactly the same
   * as the writeLong() method does.
   *
   * @param v The double precision floating point number to write to the 
   * stream.
   *
   * @exception IOException If an error occurs
   *
   * @see #writeLong(long)
   */
  public final void writeDouble (double v) throws IOException
  {
    out.writeDouble(v);
  }
  /**
   * This method writes all the bytes in a String out to the
   * stream.  One byte is written for each character in the String.
   * The high eight bits of each character are discarded.
   *
   * @param s The String to write to the stream
   *
   * @exception IOException If an error occurs
   */
  public final void writeBytes (String s) throws IOException
  {
    out.writeBytes(s);
  }
  
  /**
   * This method writes all the characters in a String to the
   * stream.  There will be two bytes for each character value.  The high
   * byte of the character will be written first.
   *
   * @param s The String to write to the stream.
   *
   * @exception IOException If an error occurs
   */
  public final void writeChars (String s) throws IOException
  {
    out.writeChars(s);
  }
  
  /**
   * This method writes a Java String to the stream in a modified
   * UTF-8 format.  First, two bytes are written to the stream indicating the
   * number of bytes to follow.  Note that this is the number of bytes in the
   * encoded String not the String length.  Next
   * come the encoded characters.  Each character in the String
   * is encoded as either one, two or three bytes.  For characters in the
   * range of \u0001 to \u007F, 
   * one byte is used.  The character
   * value goes into bits 0-7 and bit eight is 0.  For characters in the range
   * of \u0080 to \u007FF, two 
   * bytes are used.  Bits
   * 6-10 of the character value are encoded bits 0-4 of the first byte, with
   * the high bytes having a value of "110".  Bits 0-5 of the character value
   * are stored in bits 0-5 of the second byte, with the high bits set to
   * "10".  This type of encoding is also done for the null character
   * \u0000.  This eliminates any C style NUL character values
   * in the output.  All remaining characters are stored as three bytes.
   * Bits 12-15 of the character value are stored in bits 0-3 of the first
   * byte.  The high bits of the first bytes are set to "1110".  Bits 6-11
   * of the character value are stored in bits 0-5 of the second byte.  The
   * high bits of the second byte are set to "10".  And bits 0-5 of the
   * character value are stored in bits 0-5 of byte three, with the high bits
   * of that byte set to "10".
   *
   * @param s The String to write to the output in UTF format
   *
   * @exception IOException If an error occurs
   */
  public final void writeUTF (String s) throws IOException
  {
    out.writeUTF(s);
  }
  
  /**
   * This method creates a java.nio.channels.FileChannel.
   * Nio does not allow one to create a file channel directly.
   * A file channel must be created by first creating an instance of
   * Input/Output/RandomAccessFile and invoking the getChannel() method on it.
   */
  public final synchronized FileChannel getChannel ()
  {
    return ch;
  }
} // class RandomAccessFile