@@ -3,7 +3,7 @@ module Data.Buffer
3%include C "idris_buffer.h"
3%include C "idris_buffer.h"
5||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
5||| A buffer is a pointer to a sized, unstructured, mutable chunk of memory.
6−||| There are primitive operations for gettng and setting bytes, ints (32 bit)
6+||| There are primitive operations for getting and setting bytes, ints (32 bit)
7||| and strings at a location in the buffer. These operations silently fail
7||| and strings at a location in the buffer. These operations silently fail
8||| if the location is out of bounds, so bounds checking should be done in
8||| if the location is out of bounds, so bounds checking should be done in
9||| advance.
9||| advance.
@@ -133,7 +133,7 @@ readBufferFromFile (FHandle h) buf max
133 pure (record { location $= (+numread) } buf)
133 pure (record { location $= (+numread) } buf)
135||| Write 'maxbytes' from the buffer from a file, returning a new
135||| Write 'maxbytes' from the buffer from a file, returning a new
136−||| buffer with the 'locaton' pointer moved along
136+||| buffer with the 'location' pointer moved along
138writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer
138writeBufferToFile : File -> Buffer -> (maxbytes : Int) -> IO Buffer
139writeBufferToFile (FHandle h) buf max
139writeBufferToFile (FHandle h) buf max