class interface KL_INPUT_STREAM_ROUTINES

feature(s) from KL_IMPORTED_INPUT_STREAM_ROUTINES
   --  Access

   INPUT_STREAM_: KL_INPUT_STREAM_ROUTINES
      --  Routines that ought to be in class INPUT_STREAM

      ensure
         input_stream_routines_not_void: Result /= Void

feature(s) from KL_IMPORTED_INPUT_STREAM_ROUTINES
   --  Type anchors

   INPUT_STREAM_TYPE: INPUT_STREAM

feature(s) from KL_INPUT_STREAM_ROUTINES
   --  Initialization

   make_file_open_read (a_filename: STRING): like INPUT_STREAM_TYPE
      --  Create a new file object with a_filename as
      --  file name and try to open it in read-only mode.
      --  is_open_read (Result) is set to True
      --  if operation was successful.

      require
         a_filename_not_void: a_filename /= Void;
         a_filename_not_empty: a_filename.count > 0
      ensure
         file_not_void: Result /= Void

feature(s) from KL_INPUT_STREAM_ROUTINES
   --  Access

   name (a_stream: like INPUT_STREAM_TYPE): STRING
      --  Name of a_stream

      require
         a_stream_void: a_stream /= Void
      ensure
         name_not_void: Result /= Void

feature(s) from KL_INPUT_STREAM_ROUTINES
   --  Status report

   is_open_read (a_stream: like INPUT_STREAM_TYPE): BOOLEAN
      --  Is a_stream open in read mode?

      require
         a_stream_void: a_stream /= Void

   is_closed (a_stream: like INPUT_STREAM_TYPE): BOOLEAN
      --  Is a_stream closed?

      require
         a_stream_void: a_stream /= Void

   end_of_input (a_stream: like INPUT_STREAM_TYPE): BOOLEAN
      --  Has an EOF been detected?

      require
         a_stream_void: a_stream /= Void;
         a_stream_is_open_read: is_open_read(a_stream)

feature(s) from KL_INPUT_STREAM_ROUTINES
   --  Status setting

   close (a_stream: like INPUT_STREAM_TYPE)
      --  Close a_stream if it is closable,
      --  let it open otherwise.

      require
         a_stream_not_void: a_stream /= Void;
         not_closed: not is_closed(a_stream)

feature(s) from KL_INPUT_STREAM_ROUTINES
   --  Input operations

   read_string (a_stream: like INPUT_STREAM_TYPE; nb_char: INTEGER): STRING
      --  Read at most nb_char characters read from a_stream.
      --  Return the characters that have actually been read.

      require
         a_stream_not_void: a_stream /= Void;
         a_stream_open_read: is_open_read(a_stream);
         nb_char_large_enough: nb_char >= 0
      ensure
         string_not_void: Result /= Void;
         string_count_small_enough: Result.count <= nb_char

   read_stream (a_stream: like INPUT_STREAM_TYPE; a_buffer: STRING; pos, nb_char: INTEGER): INTEGER
      --  Fill a_buffer, starting at position pos with
      --  at most nb_char characters read from a_stream.
      --  Return the number of characters actually read.

      require
         a_stream_not_void: a_stream /= Void;
         a_stream_open_read: is_open_read(a_stream);
         a_buffer_not_void: a_buffer /= Void;
         valid_position: a_buffer.valid_index(pos);
         nb_char_large_enough: nb_char >= 0;
         nb_char_small_enough: nb_char <= a_buffer.count - pos + 1
      ensure
         nb_char_read_large_enough: Result >= 0;
         nb_char_read_small_enough: Result <= nb_char


end of KL_INPUT_STREAM_ROUTINES