Agda.Position

Documentation

newtype ToOffset

Positon => Offset convertion

Constructors

ToOffset

Fields

• unToOffset :: IntMap Int

makeToOffset :: Text -> ToOffset

Return a list of offsets of linebreaks ("n", "r" or "rn")

toOffset :: ToOffset -> (Int, Int) -> Int

(line, col) => offset (zero-based)

newtype FromOffset

Offset => Position convertion

Constructors

FromOffset

Fields

• unFromOffset :: IntMap Int

makeFromOffset :: Text -> FromOffset

fromOffset :: FromOffset -> Int -> (Int, Int)

toAgdaPositionWithoutFile :: ToOffset -> Position -> PositionWithoutFile

LSP Position -> Agda PositionWithoutFile

toAgdaRange :: ToOffset -> Text -> Range -> Range

LSP source locations => Agda source locations

LSP Range -> Agda Range

prettyPositionWithoutFile :: PositionWithoutFile -> String