Safe Haskell	None
Language	Haskell2010

Agda.Interaction.Highlighting.Range

Description

Ranges.

Synopsis

Documentation

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

Instances details

EmbPrj Range Source #
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Range -> S Int32 Source # icod_ :: Range -> S Int32 Source # value :: Int32 -> R Range Source #
Null Range Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods empty :: Range Source # null :: Range -> Bool Source #
NFData Range Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods rnf :: Range -> ()
Show Range Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods showsPrec :: Int -> Range -> ShowS show :: Range -> String showList :: [Range] -> ShowS
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

The Range invariant.

Zero or more consecutive and separated ranges.

Constructors

Instances details

NFData Ranges Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods rnf :: Ranges -> ()
Show Ranges Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods showsPrec :: Int -> Ranges -> ShowS show :: Ranges -> String showList :: [Ranges] -> ShowS
Eq Ranges Source #
Instance details Defined in Agda.Interaction.Highlighting.Range Methods (==) :: Ranges -> Ranges -> Bool (/=) :: Ranges -> Ranges -> Bool

The Ranges invariant.

True iff the ranges overlap.

The ranges are assumed to be well-formed.

Converts a range to a list of positions.

Converts several ranges to a list of positions.

Converts a Range to a Ranges.

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

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.