class interface ES_LINE_SEPARATOR
   -- 
   --  Breaks a unformatted stream into individual lines. Assumes
   --  it will be working with an asynchronous input.
   -- 

creation
   make
      --  Create a separator.

feature(s) from KL_IMPORTED_STRING_ROUTINES
   --  Access

   string_: KL_STRING_ROUTINES
      --  Routines that ought to be in class STRING
      ensure
         string_routines_not_void: Result /= Void

feature(s) from ES_LINE_SEPARATOR
   --  Accessors

   has_full_lines: BOOLEAN
      --  Are there one or more full lines currently in the separator?

   item: STRING
      --  The next line
      require
         right_time: has_full_lines
      ensure
         not_void: Result /= Void;
         newline_removed: not Result.has('%N') and not Result.has('%R')

   empty: BOOLEAN
      --  Is the separator entirely empty?

   has_residue: BOOLEAN
      --  Is there residue remaining?
      require
         valid_time: not has_full_lines

   residue: STRING
      --  The remaining data
      require
         valid_time: not has_full_lines;
         some_present: has_residue
      ensure
         not_line: not Result.has('%N') and not Result.has('%R')

feature(s) from ES_LINE_SEPARATOR
   --  Modifiers

   put (data: STRING)
      --  Adds data to the internal buffer.
      require
         not_void: data /= Void
      ensure
         not_empty: not data.empty implies not empty

   forth
      --  Advance to the next new line
      require
         right_time: has_full_lines

invariant

    has_full_lines: has_full_lines = last_index_position <= buffer.count;

    buffer_present: buffer /= Void;

    sanity: has_full_lines or else has_residue implies not empty;

    indeces: first_index_position <= last_index_position;

    non_negative: first_index_position >= 1 and last_index_position >= 1;

    on_newline: has_full_lines implies considered_new_line(buffer @ last_index_position);

    off_data: not has_full_lines implies last_index_position = buffer.count + 1;

end of ES_LINE_SEPARATOR