package grace
Install
dune-project
Dependency
Authors
Maintainers
Sources
sha256=388149857c0fbaf2489b1e396af25aadd6185998847b75570f9198a077ad1ace
sha512=9ffa701f7729f90976594c4ec77b968f15450d8d7a1f0c65fe60d092c136b18f1c8bbd5f5772a651c925dabcdc82ac7023c30a4caa1b94e3e158ef2efa34b85e
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.