class interface ES_BUFFER
   -- 
   --  Provides an external memory buffer to managed by Eiffel, but used
   --  by native machine code, probably C.
   -- 

creation
   make (size: INTEGER)
      --  Make a buffer of size.
      require
         positive: size > 0
      ensure
         capacity_set: capacity = size;
         buffer_present: pointer /= default_pointer

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 KL_SHARED_EXCEPTIONS
   --  Access

   exceptions: KL_EXCEPTIONS
      --  Exception handling
      ensure
         exceptions_not_void: Result /= Void

feature(s) from MEMORY
   --  Status Report :

   collecting: BOOLEAN
      --  Is garbage collection enabled ?

feature(s) from MEMORY
   --  Status setting :

   collection_off
      --  Disable garbage collection.

   collection_on
      --  Enable garbage collection.

feature(s) from MEMORY
   --  Removal :

   dispose
      --  Free the C side

   full_collect
      --  Force a full collection cycle if garbage collection is
      --  enabled; do nothing otherwise.

feature(s) from MEMORY
   --  The Guru section (low level memory management) :

   pointer_size: INTEGER
      --  The size in number of bytes for a pointer.

feature(s) from ES_IMPORTED_EXTERNALS
   --  Once

   externals_: ES_EXTERNALS
      --  Access those compatability commands.

feature(s) from ES_BUFFER
   --  Accessors

   capacity: INTEGER
      --  The size of the buffer

   pointer: POINTER
      --  The buffer itself

   item (which: INTEGER): CHARACTER
      --  The character (byte) at offset which
      require
         good_index: which >= 0 and which < capacity

   string (first, last: INTEGER): STRING
      --  The string, copied from Current, at offsets first .. last
      require
         good_index: first >= 0 and last >= 0 and first <= last and last < capacity
      ensure
         result_present: Result /= Void;
         correct_size: Result.count = last - first + 1

feature(s) from ES_BUFFER
   --  Modifiers

   put (what: CHARACTER; which: INTEGER)
      --  Put what into position which in Current. The 
      --  remainder is unchanged.
      require
         good_index: which >= 0 and which < capacity
      ensure
         set: item(which) = what

   put_string (what: STRING; start, which, count: INTEGER)
      --  Put count characters from start within what into 
      --  Current, starting at position which.
      require
         not_void: what /= Void;
         good_buffer_index: which >= 0 and which + count <= capacity;
         good_string_index: start >= 1 and start + count <= what.count + 1

   resize (new_size: INTEGER)
      --  Change the buffer size. Preserves what it can.
      require
         positive: new_size > 0
      ensure
         not_void: pointer /= default_pointer;
         correct_size: capacity = new_size


end of ES_BUFFER