| Agda-2.2.6: A dependently typed functional programming language and proof assistant | Source code | Contents | Index

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 |

Instances

Eq Range
Data Range
Ord Range
Show Range
Typeable Range
Arbitrary Range
CoArbitrary Range
EmbPrj Range

rangeInvariant :: Range -> Bool | Source

The `Range` invariant.

overlapping :: Range -> Range -> Bool | Source

`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 `QName`s. 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 `Range`s.

tests :: IO Bool | Source

All the properties.
Produced by Haddock version 2.4.2