Agda.Interaction.Highlighting.Range

Ranges.

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, to :: !Int

Instances

EmbPrj Range

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Methods

icode :: Range -> S Int32

icod_ :: Range -> S Int32

value :: Int32 -> R Range

Null Range

Defined in Agda.Interaction.Highlighting.Range

Methods

empty :: Range

null :: Range -> Bool

Show Range

Defined in Agda.Interaction.Highlighting.Range

Methods

showsPrec :: Int -> Range -> ShowS

show :: Range -> String

showList :: [Range] -> ShowS

NFData Range

Defined in Agda.Interaction.Highlighting.Range

Methods

rnf :: Range -> ()

Eq Range

Defined in Agda.Interaction.Highlighting.Range

Methods

(==) :: Range -> Range -> Bool

(/=) :: Range -> Range -> Bool

Ord Range

Defined in Agda.Interaction.Highlighting.Range

Methods

compare :: Range -> Range -> Ordering

(<) :: Range -> Range -> Bool

(<=) :: Range -> Range -> Bool

(>) :: Range -> Range -> Bool

(>=) :: Range -> Range -> Bool

max :: Range -> Range -> Range

min :: Range -> Range -> Range

rangeInvariant :: Range -> Bool

The Range invariant.

newtype Ranges

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range]

Instances

Show Ranges

Defined in Agda.Interaction.Highlighting.Range

Methods

showsPrec :: Int -> Ranges -> ShowS

show :: Ranges -> String

showList :: [Ranges] -> ShowS

NFData Ranges

Defined in Agda.Interaction.Highlighting.Range

Methods

rnf :: Ranges -> ()

Eq Ranges

Defined in Agda.Interaction.Highlighting.Range

Methods

(==) :: Ranges -> Ranges -> Bool

(/=) :: Ranges -> Ranges -> Bool

rangesInvariant :: Ranges -> Bool

The Ranges invariant.

overlapping :: Range -> Range -> Bool

True iff the ranges overlap.

The ranges are assumed to be well-formed.

overlappings :: Ranges -> Ranges -> Bool

empty :: Null a => a

rangeToPositions :: Range -> [Int]

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Int]

Converts several ranges to a list of positions.

rToR :: Range -> Ranges

Converts a Range' to a Ranges.

rangeToRange :: Range -> Range

Converts a Range', seen as a continuous range, to a Range.

minus :: Ranges -> Ranges -> Ranges

minus xs ys computes the difference between xs and ys: the result contains those positions which are present in xs but not in ys.

Linear in the lengths of the input ranges.