Text.ByteRange

Conversion of the bounds of a byte sequence to an text
sequence plus absolute and relative bounds for pretty printing
errors when streaming large files.

Reexports

Definitions

record Chunk : Type

  A non-empty chunk of bytes in a sequence or stream of bytes
  wrapped up with some counters.

Totality: total
Visibility: public export
Constructor: 

CH : (bytes : ByteString) -> BytePos -> Nat -> Nat -> {auto 0 _ : IsSucc (bytes .size)} -> Chunk

Projections:

.bytes : Chunk -> ByteString

  The current chunk of bytes

.first : Chunk -> BytePos

  Absolute byte position of the first byte in `bytes`

.lines : Chunk -> Nat

  Number of line breaks in this chunk

.linesBefore : Chunk -> Nat

  Number of line breaks encountered before this chunk

0 .prf : ({rec:0} : Chunk) -> IsSucc ((bytes {rec:0}) .size)

Hints:

Show Chunk

Show Chunk

.bytes : Chunk -> ByteString

  The current chunk of bytes

Totality: total
Visibility: public export

bytes : Chunk -> ByteString

  The current chunk of bytes

Totality: total
Visibility: public export

.first : Chunk -> BytePos

  Absolute byte position of the first byte in `bytes`

Totality: total
Visibility: public export

first : Chunk -> BytePos

  Absolute byte position of the first byte in `bytes`

Totality: total
Visibility: public export

.linesBefore : Chunk -> Nat

  Number of line breaks encountered before this chunk

Totality: total
Visibility: public export

linesBefore : Chunk -> Nat

  Number of line breaks encountered before this chunk

Totality: total
Visibility: public export

.lines : Chunk -> Nat

  Number of line breaks in this chunk

Totality: total
Visibility: public export

lines : Chunk -> Nat

  Number of line breaks in this chunk

Totality: total
Visibility: public export

0 .prf : ({rec:0} : Chunk) -> IsSucc ((bytes {rec:0}) .size)

Totality: total
Visibility: public export

0 prf : ({rec:0} : Chunk) -> IsSucc ((bytes {rec:0}) .size)

Totality: total
Visibility: public export

.last : Chunk -> BytePos

  Absolute position of the last byte in the given `Chunk`.

Totality: total
Visibility: export

.next : Chunk -> BytePos

  Absolute position of the first byte of the next chunk after this one.

Totality: total
Visibility: export

.linesIncluding : Chunk -> Nat

  Number of linebreaks up to and including the given chunk.

Totality: total
Visibility: export

nextChunk : Maybe Chunk -> (bs : ByteString) -> {auto 0 _ : IsSucc (bs .size)} -> Chunk

  Given an optional previous chunk plus a non-empty byte vector,
  computes the stats of the current chunk.

Totality: total
Visibility: export

data ByteRange : Type

  A sequence of chunks, describing if it holds some start
  and end position.

Totality: total
Visibility: public export
Constructors:

Prefix : SnocList Chunk -> ByteRange

Start : SnocList Chunk -> ByteRange

End : SnocList Chunk -> ByteRange

Done : SnocList Chunk -> ByteRange

None : ByteRange

Hints:

Show ByteRange

Show ByteRange

isDone : ByteRange -> Bool

Totality: total
Visibility: export

chunks : ByteRange -> SnocList Chunk

Totality: total
Visibility: export

appendChunk : BytePos -> BytePos -> ByteRange -> ByteString -> ByteRange

  Given a start and end position, appends a chunk of bytes to
  range of bytes, making sure that the range will contain
  enough lines before the start byte and enough lines after the
  end byte.

Totality: total
Visibility: export

enclosingBytes : Foldable f => BytePos -> BytePos -> f ByteString -> ByteRange

  Given a sequence (or stream) of byte vectors, we want to find
  a minimal chunk fully enclosing a given byte range, so that we
  can pretty print that byte range.
  
  The chunk should fulfill the following prerequisites:
   * fully contain all bytes given in the byte range
   * contain the last five line breaks before the first
     byte in the byte range, or - if there are not as many line breaks before
     the first byte - contain the first byte of the whole byte stream
     so that we can print the whole line where - for instance -
     an error occurred
   * contain at least the next line-break *after* the last position (if any)

Totality: total
Visibility: export

record TextBounds : Type

  Absolute and relative text bounds in a stream of byte vectors

Totality: total
Visibility: public export
Constructor: 

TB : String -> Bounds -> Bounds -> TextBounds

Projections:

.absolute : TextBounds -> Bounds

  Absolute bounds of the start and end position of the given
  byte sequence.

.content : TextBounds -> String

  An excerpt of the byte stream large enough to fully contain
  a given byte sequence

.relative : TextBounds -> Bounds

  Relative bounds of the start and end position of the given
  byte sequence.

Hints:

Eq TextBounds

Eq TextBounds

Show TextBounds

Show TextBounds

.content : TextBounds -> String

  An excerpt of the byte stream large enough to fully contain
  a given byte sequence

Totality: total
Visibility: public export

content : TextBounds -> String

  An excerpt of the byte stream large enough to fully contain
  a given byte sequence

Totality: total
Visibility: public export

.absolute : TextBounds -> Bounds

  Absolute bounds of the start and end position of the given
  byte sequence.

Totality: total
Visibility: public export

absolute : TextBounds -> Bounds

  Absolute bounds of the start and end position of the given
  byte sequence.

Totality: total
Visibility: public export

.relative : TextBounds -> Bounds

  Relative bounds of the start and end position of the given
  byte sequence.

Totality: total
Visibility: public export

relative : TextBounds -> Bounds

  Relative bounds of the start and end position of the given
  byte sequence.

Totality: total
Visibility: public export

textBounds : BytePos -> BytePos -> ByteRange -> Maybe TextBounds

  Given a byte range that is supposed to contain the
  byte sequence corresponding to the given byte bounds,
  returns the proper text bounds - or `Nothing` if
  something went wrong.

Totality: total
Visibility: export

toFCErr : ByteError e -> TextBounds -> FCErr e

Totality: total
Visibility: export