Agda-2.2.6: A dependently typed functional programming language and proof assistantSource codeContentsIndex
Agda.Interaction.Highlighting.Range
Description
Ranges.
Synopsis
data Range = Range {
from :: Integer
to :: Integer
}
rangeInvariant :: Range -> Bool
overlapping :: Range -> Range -> Bool
toList :: Range -> [Integer]
getRanges :: Name -> ([Range], Bool)
getRangesA :: QName -> ([Range], Bool)
rToR :: Range -> [Range]
tests :: IO Bool
Documentation
data Range Source

Character ranges. The first character in the file has position 1. Note that the to position is considered to be outside of the range.

Invariant: from <= to.

Constructors
Range
from :: Integer
to :: Integer
rangeInvariant :: Range -> BoolSource
The Range invariant.
overlapping :: Range -> Range -> BoolSource

True iff the ranges overlap.

The ranges are assumed to be well-formed.

toList :: Range -> [Integer]Source
Converts a range to a list of positions.
getRanges :: Name -> ([Range], Bool)Source

Calculates a set of ranges associated with a name.

For an operator the ranges associated with the NameParts are returned. Otherwise the range associated with the Name is returned.

A boolean, indicating operatorness, is also returned.

getRangesA :: QName -> ([Range], Bool)Source
Like getRanges, but for QNames. Note that the module part of the name is thrown away; only the base part is used.
rToR :: Range -> [Range]Source
Converts a Range to a list of Ranges.
tests :: IO BoolSource
All the properties.
Produced by Haddock version 2.6.0