Agda-2.6.3.20230914: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

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 

Fields

Instances

Instances details
EmbPrj Range Source # 
Instance details

Defined in Agda.TypeChecking.Serialise.Instances.Highlighting

Null Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Show Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

showsPrec :: Int -> Range -> ShowS #

show :: Range -> String #

showList :: [Range] -> ShowS #

NFData Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

rnf :: Range -> () #

Eq Range Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

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

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

Ord Range Source # 
Instance details

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 Source #

The Range invariant.

newtype Ranges Source #

Zero or more consecutive and separated ranges.

Constructors

Ranges [Range] 

Instances

Instances details
Show Ranges Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

NFData Ranges Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

rnf :: Ranges -> () #

Eq Ranges Source # 
Instance details

Defined in Agda.Interaction.Highlighting.Range

Methods

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

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

overlapping :: Range -> Range -> Bool Source #

True iff the ranges overlap.

The ranges are assumed to be well-formed.

empty :: Null a => a Source #

rangeToPositions :: Range -> [Int] Source #

Converts a range to a list of positions.

rangesToPositions :: Ranges -> [Int] Source #

Converts several ranges to a list of positions.

rToR :: Range -> Ranges Source #

Converts a Range' to a Ranges.

rangeToRange :: Range -> Range Source #

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

minus :: Ranges -> Ranges -> Ranges Source #

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.