package grace
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=19576d3f32e4a69c7ebad26a801b568a2e3bff24a0e4d5ddf3b8bf4eac479d4c
sha512=436db3699126eec797da1be9f530759547804cc081ed365a75ba8ae9b053c05999ae820d294dd20f6a68e0712084579c585105a3855d71b459efc1367172bd66
doc/grace.rendering/Grace_rendering/Source_reader/index.html
Module Grace_rendering.Source_readerSource
A source reader maintains a global table mapping source descriptors to their contents and their line starts.
A source descriptor is a handle for an open source
init () initializes the global source reader table.
clear () clears the global source reader table.
with_reader f runs f with an initialized reader table, clearing it once f returns.
open_source src opens the source, returning its descriptor.
line_starts sd returns the (possibly cached) line starts of the source sd.
length sd returns the length or size in bytes of src.
It is semantically equivalent to Source.length src.
unsafe_get sd i reads the ith byte of the source without performing any bounds checks on i.
slice sd range reads the slice of bytes defined by range.
lines sd returns an iterator over lines in source sd.
lines_in_range sd range returns an iterator over lines in the range in sd.