Text.FC

(source)

Definitions

data Origin : Type

Totality: total
Visibility: public export
Constructors:

FileSrc : String -> Origin
Virtual : Origin

Hints:

Eq Origin
Interpolation Origin
Show Origin

record FileContext : Type

Totality: total
Visibility: public export
Constructor:

FC : Origin -> Bounds -> FileContext

Projections:

.bounds : FileContext -> Bounds
.origin : FileContext -> Origin

Hints:

Eq FileContext
Interpolation FileContext
Show FileContext

.origin : FileContext -> Origin

Totality: total
Visibility: public export

origin : FileContext -> Origin

Totality: total
Visibility: public export

.bounds : FileContext -> Bounds

Totality: total
Visibility: public export

bounds : FileContext -> Bounds

Totality: total
Visibility: public export

fromBounded : Origin -> Bounded a -> (FileContext, a)

Totality: total
Visibility: public export

virtualFromBounded : Bounded a -> (FileContext, a)

Totality: total
Visibility: public export

toPosition : Nat -> ByteString -> Position

  Converts an index into a bytestring to a position
  (line and column) in the corresponding UTF-8 string.

Totality: total
Visibility: export

printFC : FileContext -> Bounds -> List String -> List String

  Pretty prints a file context, highlighting the section in the given
  list of source lines.
  
  The `FileContext` describes the absolute context (file source and
  bounds) where an error occurred, while `relBounds` is the error's
  position relative to the given list of lines.
  
  The above distinction is necessary when streaming large amounts of
  data, where it is not feasible to keep the whole data in memory but
  only the most recent chunk.

Totality: total
Visibility: export