Agda-2.2.10: A dependently typed functional programming language and proof assistant

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

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 |

Fields

from :: Integer
to :: Integer

Instances

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

rangeInvariant :: Range -> Bool

The `Range` invariant.

overlapping :: Range -> Range -> Bool

`True` iff the ranges overlap.

The ranges are assumed to be well-formed.

toList :: Range -> [Integer]

Converts a range to a list of positions.

getRanges :: Name -> ([Range], Bool)

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)

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]

Converts a `Range` to a list of `Range`s.

tests :: IO Bool

All the properties.