class interface MINI_PARSER_BUFFER
   --
   -- Useful and efficient mini parsing buffer.
   -- From the user point of view, an object of this class can be considered 
   -- as the combination of a STRING to be parsed with an extra INTEGER 
   -- index to memorize the current position in this STRING. 
   -- Beside the fact that this object provides the current position 
   -- memorization inside the STRING to be parsed, the implementation is 
   -- also more efficient than the one you may get by using the traditional 
   -- STRING interface.
   --

feature(s) from MINI_PARSER_BUFFER   initialize_with (string: STRING)
      -- Initialize the Current buffer using the content of the 
      -- string.

      require
         string /= Void
      ensure
         count = string.count;
         last_error = Void

   count: INTEGER
      -- The length of the Current buffer which is also the maximum 
      -- valid index.


   current_index: INTEGER
      -- Index of the current character.


   current_character: CHARACTER
      -- The current character (the one at current_index).

      require
         current_index.in_range(1,count)

   end_reached: BOOLEAN
      -- Is the end of the buffer reached?

      ensure
         Result = (current_index > count)

   next
      -- Move the current_index forward by one.

      require
         not end_reached
      ensure
         current_index = 1 + old current_index

   skip_separators
      -- Skip all separators by using is_separator of class CHARACTER.


   last_error: STRING
      -- Can be used to memorize an error message.


   set_last_error (error_msg: like last_error)
      ensure
         last_error = error_msg



end of MINI_PARSER_BUFFER