package grace
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=821df54882c9253eac69f47bcf3a71ffdc61c77fdae42587c32aada5b56cfeae
sha512=007afa83251da3ddecd874e120ea89dce0253c387a64a5fece69069d3486ec5eb6c82d6bf0febaf23dd322bd9eaadc2f7882e33f05a2e1fa18a41294e7dc3ba1
doc/grace.source_reader/Grace_source_reader/index.html
Module Grace_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.