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

Safe HaskellSafe-Infered

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

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
 

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 QNames. 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 Ranges.

tests :: IO Bool

All the properties.