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

Safe Haskell | None
Language | Haskell2010

Agda.Interaction.Highlighting.Precise

Contents

- Highlighting information
  - Operations
- Orphan instances

Description

Types used for precise syntax highlighting.

Synopsis

- data Aspect
  - = Comment
  - | Keyword
  - | String
  - | Number
  - | Hole
  - | Symbol
  - | PrimitiveType
  - | Name (Maybe NameKind) Bool
  - | Pragma
  - | Background
  - | Markup
- data NameKind
  - = Bound
  - | Generalizable
  - | Constructor Induction
  - | Datatype
  - | Field
  - | Function
  - | Module
  - | Postulate
  - | Primitive
  - | Record
  - | Argument
  - | Macro
- data OtherAspect
  - = Error
  - | ErrorWarning
  - | DottedPattern
  - | UnsolvedMeta
  - | UnsolvedConstraint
  - | TerminationProblem
  - | PositivityProblem
  - | Deadcode
  - | ShadowingInTelescope
  - | CoverageProblem
  - | IncompletePattern
  - | TypeChecks
  - | MissingDefinition
  - | InstanceProblem
  - | CosmeticProblem
  - | CatchallClause
  - | ConfluenceProblem
- data Aspects = Aspects {
  - aspect :: Maybe Aspect
  - otherAspects :: Set OtherAspect
  - note :: String
  - definitionSite :: Maybe DefinitionSite
  - tokenBased :: !TokenBased
  }
- data DefinitionSite = DefinitionSite {
  - defSiteModule :: TopLevelModuleName' Range
  - defSitePos :: Int
  - defSiteHere :: Bool
  - defSiteAnchor :: Maybe String
  }
- data TokenBased
  - = TokenBased
  - | NotOnlyTokenBased
- newtype RangePair = RangePair {
  - rangePair :: (Ranges, Aspects)
  }
- rangePairInvariant :: RangePair -> Bool
- newtype PositionMap = PositionMap {
  - positionMap :: IntMap Aspects
  }
- newtype DelayedMerge hl = DelayedMerge (Endo [hl])
- delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool
- type HighlightingInfo = RangeMap Aspects
- highlightingInfoInvariant :: HighlightingInfo -> Bool
- type HighlightingInfoBuilder = DelayedMerge RangePair
- highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool
- parserBased :: Aspects
- kindOfNameToNameKind :: KindOfName -> NameKind
- class IsBasicRangeMap a m | m -> a where
  - singleton :: Ranges -> a -> m
  - toMap :: m -> IntMap a
  - toList :: m -> [(Range, a)]
  - coveringRange :: m -> Maybe Range
- several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl
- class Convert a b where
  - convert :: a -> b
- insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a)
- restrictTo :: Range -> RangeMap a -> RangeMap a

# Highlighting information

data Aspect Source #

Constructors

Comment |
Keyword |
String |
Number |
Hole |
Symbol | Symbols like forall, =, ->, etc.
PrimitiveType | Things like Set and Prop.
Name (Maybe NameKind) Bool | Is the name an operator part?
Pragma | Text occurring in pragmas that does not have a more specific aspect.
Background | Non-code contents in literate Agda
Markup | Delimiters used to separate the Agda code blocks from the other contents in literate Agda

#### Instances

Instances details

EmbPrj Aspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspect -> S Word32 Source # icod_ :: Aspect -> S Word32 Source # value :: Word32 -> R Aspect Source #
NFData Aspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspect -> () Source #
Semigroup Aspect Source # | `NameKind` in `Name` can get more precise.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: Aspect -> Aspect -> Aspect Source # sconcat :: NonEmpty Aspect -> Aspect Source # stimes :: Integral b => b -> Aspect -> Aspect Source #
Generic Aspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspect |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: Aspect -> Rep Aspect x Source #

to :: Rep Aspect x -> Aspect Source #

Show Aspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspect -> ShowS Source # show :: Aspect -> String Source # showList :: [Aspect] -> ShowS Source #
Eq Aspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspect -> Aspect -> Bool Source # (/=) :: Aspect -> Aspect -> Bool Source #
type Rep Aspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "Comment" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Keyword" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "String" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Number" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Hole" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Symbol" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "PrimitiveType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Name" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe NameKind)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))) :+: (C1 ('MetaCons "Pragma" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Background" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Markup" 'PrefixI 'False) (U1 :: Type -> Type)))))

data NameKind Source #

`NameKind`s are figured out during scope checking.

Constructors

Bound | Bound variable.
Generalizable | Generalizable variable. (This includes generalizable variables that have been generalized).
Constructor Induction | Inductive or coinductive constructor.
Datatype |
Field | Record field.
Function |
Module | Module name.
Postulate |
Primitive | Primitive.
Record | Record type.
Argument | Named argument, like x in {x = v}
Macro | Macro.

#### Instances

Instances details

EmbPrj NameKind Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: NameKind -> S Word32 Source # icod_ :: NameKind -> S Word32 Source # value :: Word32 -> R NameKind Source #
NFData NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods rnf :: NameKind -> () Source #
Semigroup NameKind Source # | Some `NameKind`s are more informative than others.
Instance details Defined in Agda.Syntax.Common.Aspect Methods (<>) :: NameKind -> NameKind -> NameKind Source # sconcat :: NonEmpty NameKind -> NameKind Source # stimes :: Integral b => b -> NameKind -> NameKind Source #
Generic NameKind Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep NameKind |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

Methods

from :: NameKind -> Rep NameKind x Source #

to :: Rep NameKind x -> NameKind Source #

Show NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> NameKind -> ShowS Source # show :: NameKind -> String Source # showList :: [NameKind] -> ShowS Source #
Eq NameKind Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: NameKind -> NameKind -> Bool Source # (/=) :: NameKind -> NameKind -> Bool Source #
type Rep NameKind Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (((C1 ('MetaCons "Bound" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Generalizable" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Constructor" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Induction)))) :+: (C1 ('MetaCons "Datatype" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Field" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Function" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: ((C1 ('MetaCons "Module" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Postulate" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Primitive" 'PrefixI 'False) (U1 :: Type -> Type))) :+: (C1 ('MetaCons "Record" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Argument" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Macro" 'PrefixI 'False) (U1 :: Type -> Type)))))

data OtherAspect Source #

Other aspects, generated by type checking. (These can overlap with each other and with `Aspect`s.)

Constructors

Error |
ErrorWarning | A warning that is considered fatal in the end.
DottedPattern |
UnsolvedMeta |
UnsolvedConstraint | Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.
TerminationProblem |
PositivityProblem |
Deadcode | Used for highlighting unreachable clauses, unreachable RHS (because of an absurd pattern), etc.
ShadowingInTelescope | Used for shadowed repeated variable names in telescopes.
CoverageProblem |
IncompletePattern | When this constructor is used it is probably a good idea to include a `note` explaining why the pattern is incomplete.
TypeChecks | Code which is being type-checked.
MissingDefinition | Function declaration without matching definition.
InstanceProblem | Unusable instance etc.
CosmeticProblem | Nothing serious, just a beauty flaw.
CatchallClause |
ConfluenceProblem |

#### Instances

Instances details

EmbPrj OtherAspect Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Word32 Source # icod_ :: OtherAspect -> S Word32 Source # value :: Word32 -> R OtherAspect Source #
NFData OtherAspect Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: OtherAspect -> () Source #
Bounded OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods minBound :: OtherAspect Source # maxBound :: OtherAspect Source #
Enum OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

succ :: OtherAspect -> OtherAspect Source #

pred :: OtherAspect -> OtherAspect Source #

toEnum :: Int -> OtherAspect Source #

fromEnum :: OtherAspect -> Int Source #

enumFrom :: OtherAspect -> [OtherAspect] Source #

enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect] Source #

enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect] Source #

Generic OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep OtherAspect |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosmeticProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type))))))

Methods

from :: OtherAspect -> Rep OtherAspect x Source #

to :: Rep OtherAspect x -> OtherAspect Source #

Show OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> OtherAspect -> ShowS Source # show :: OtherAspect -> String Source # showList :: [OtherAspect] -> ShowS Source #
Eq OtherAspect Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: OtherAspect -> OtherAspect -> Bool Source # (/=) :: OtherAspect -> OtherAspect -> Bool Source #
Ord OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Methods

compare :: OtherAspect -> OtherAspect -> Ordering Source #

(<) :: OtherAspect -> OtherAspect -> Bool Source #

(<=) :: OtherAspect -> OtherAspect -> Bool Source #

(>) :: OtherAspect -> OtherAspect -> Bool Source #

(>=) :: OtherAspect -> OtherAspect -> Bool Source #

max :: OtherAspect -> OtherAspect -> OtherAspect Source #

min :: OtherAspect -> OtherAspect -> OtherAspect Source #

type Rep OtherAspect Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) ((((C1 ('MetaCons "Error" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ErrorWarning" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "DottedPattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "UnsolvedMeta" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "UnsolvedConstraint" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TerminationProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "PositivityProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Deadcode" 'PrefixI 'False) (U1 :: Type -> Type)))) :+: (((C1 ('MetaCons "ShadowingInTelescope" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "CoverageProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "IncompletePattern" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TypeChecks" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "MissingDefinition" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "InstanceProblem" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "CosmeticProblem" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type))))))

data Aspects Source #

Syntactic aspects of the code. (These cannot overlap.)

Meta information which can be associated with a character/character range.

Constructors

Aspects |

Fields

- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String

  This note, if not null, can be displayed as a tool-tip or something like that. It should contain useful information about the range (like the module containing a certain identifier, or the fixity of an operator).

- definitionSite :: Maybe DefinitionSite

  The definition site of the annotated thing, if applicable and known.

- tokenBased :: !TokenBased

  Is this entry token-based?

#### Instances

Instances details

EncodeTCM Doc Source # |
Instance details Defined in Agda.Interaction.JSON Methods encodeTCM :: Doc -> TCM Value Source #
Underscore Doc Source # |
Instance details Defined in Agda.Syntax.Common Methods underscore :: Doc Source # isUnderscore :: Doc -> Bool Source #
ReportS Doc Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m () Source #
TraceS Doc Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> Doc -> m c -> m c Source #
EmbPrj Aspects Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: Aspects -> S Word32 Source # icod_ :: Aspects -> S Word32 Source # value :: Word32 -> R Aspects Source #
EmbPrj Doc Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Errors Methods icode :: Doc -> S Word32 Source # icod_ :: Doc -> S Word32 Source # value :: Word32 -> R Doc Source #
ToJSON Doc Source # |
Instance details Defined in Agda.Interaction.JSON Methods toJSON :: Doc -> Value Source # toEncoding :: Doc -> Encoding Source # toJSONList :: [Doc] -> Value Source # toEncodingList :: [Doc] -> Encoding Source # omitField :: Doc -> Bool Source #
NFData Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: Aspects -> () Source #
Monoid Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: Aspects Source # mappend :: Aspects -> Aspects -> Aspects Source # mconcat :: [Aspects] -> Aspects Source #
Semigroup Aspects Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: Aspects -> Aspects -> Aspects Source # sconcat :: NonEmpty Aspects -> Aspects Source # stimes :: Integral b => b -> Aspects -> Aspects Source #
Generic Aspects Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep Aspects |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

Methods

from :: Aspects -> Rep Aspects x Source #

to :: Rep Aspects x -> Aspects Source #

Show Aspects Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> Aspects -> ShowS Source # show :: Aspects -> String Source # showList :: [Aspects] -> ShowS Source #
Eq Aspects Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: Aspects -> Aspects -> Bool Source # (/=) :: Aspects -> Aspects -> Bool Source #
IsBasicRangeMap Aspects PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
Convert PositionMap (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
ReportS (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m () Source #
ReportS [Doc] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m () Source #
ReportS [TCM Doc] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods reportS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m () Source #
TraceS (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m c -> m c Source #
TraceS [Doc] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [Doc] -> m c -> m c Source #
TraceS [TCM Doc] Source # |
Instance details Defined in Agda.TypeChecking.Monad.Debug Methods traceS :: MonadDebug m => VerboseKey -> VerboseLevel -> [TCM Doc] -> m c -> m c Source #
Null (TCM Doc) Source # |
Instance details Defined in Agda.TypeChecking.Monad.Base Methods empty :: TCM Doc Source # null :: TCM Doc -> Bool Source #
Semigroup (TCM Doc) Source # | This instance is more specific than a generic instance `Semigroup a => Semigroup (TCM a)`.
Instance details Defined in Agda.TypeChecking.Pretty Methods (<>) :: TCM Doc -> TCM Doc -> TCM Doc Source # sconcat :: NonEmpty (TCM Doc) -> TCM Doc Source # stimes :: Integral b => b -> TCM Doc -> TCM Doc Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #
Convert (RangeMap Aspects) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: RangeMap Aspects -> RangeMap Aspects Source #
Monad m => Null (PureConversionT m Doc) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods empty :: PureConversionT m Doc Source # null :: PureConversionT m Doc -> Bool Source #
type Rep Aspects Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep Aspects = D1 ('MetaData "Aspects" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "Aspects" 'PrefixI 'True) ((S1 ('MetaSel ('Just "aspect") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Aspect)) :*: S1 ('MetaSel ('Just "otherAspects") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Set OtherAspect))) :*: (S1 ('MetaSel ('Just "note") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 String) :*: (S1 ('MetaSel ('Just "definitionSite") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe DefinitionSite)) :*: S1 ('MetaSel ('Just "tokenBased") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 TokenBased)))))

data DefinitionSite Source #

Constructors

DefinitionSite |

Fields

- defSiteModule :: TopLevelModuleName' Range

  The defining module.

- defSitePos :: Int

  The file position in that module. File positions are counted from 1.

- defSiteHere :: Bool

  Has this `DefinitionSite` been created at the defining site of the name?

- defSiteAnchor :: Maybe String

  A pretty name for the HTML linking.

#### Instances

Instances details

EmbPrj DefinitionSite Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Word32 Source # icod_ :: DefinitionSite -> S Word32 Source # value :: Word32 -> R DefinitionSite Source #
NFData DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: DefinitionSite -> () Source #
Semigroup DefinitionSite Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite Source # sconcat :: NonEmpty DefinitionSite -> DefinitionSite Source # stimes :: Integral b => b -> DefinitionSite -> DefinitionSite Source #
Generic DefinitionSite Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

Associated Types

type Rep DefinitionSite |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

Methods

from :: DefinitionSite -> Rep DefinitionSite x Source #

to :: Rep DefinitionSite x -> DefinitionSite Source #

Show DefinitionSite Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> DefinitionSite -> ShowS Source # show :: DefinitionSite -> String Source # showList :: [DefinitionSite] -> ShowS Source #
Eq DefinitionSite Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: DefinitionSite -> DefinitionSite -> Bool Source # (/=) :: DefinitionSite -> DefinitionSite -> Bool Source #
type Rep DefinitionSite Source # |

Instance details

Defined in Agda.Syntax.Common.Aspect

type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Syntax.Common.Aspect" "Agda-2.8.0-DJrTbcOFazJDzri4fKrI2F" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (TopLevelModuleName' Range)) :*: S1 ('MetaSel ('Just "defSitePos") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int)) :*: (S1 ('MetaSel ('Just "defSiteHere") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: S1 ('MetaSel ('Just "defSiteAnchor") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe String)))))

data TokenBased Source #

Is the highlighting "token-based", i.e. based only on information from the lexer?

Constructors

TokenBased |
NotOnlyTokenBased |

#### Instances

Instances details

EncodeTCM TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods encodeTCM :: TokenBased -> TCM Value Source #
EmbPrj TokenBased Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: TokenBased -> S Word32 Source # icod_ :: TokenBased -> S Word32 Source # value :: Word32 -> R TokenBased Source #
ToJSON TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.JSON Methods toJSON :: TokenBased -> Value Source # toEncoding :: TokenBased -> Encoding Source # toJSONList :: [TokenBased] -> Value Source # toEncodingList :: [TokenBased] -> Encoding Source # omitField :: TokenBased -> Bool Source #
Monoid TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: TokenBased Source # mappend :: TokenBased -> TokenBased -> TokenBased Source # mconcat :: [TokenBased] -> TokenBased Source #
Semigroup TokenBased Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: TokenBased -> TokenBased -> TokenBased Source # sconcat :: NonEmpty TokenBased -> TokenBased Source # stimes :: Integral b => b -> TokenBased -> TokenBased Source #
Show TokenBased Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods showsPrec :: Int -> TokenBased -> ShowS Source # show :: TokenBased -> String Source # showList :: [TokenBased] -> ShowS Source #
Eq TokenBased Source # |
Instance details Defined in Agda.Syntax.Common.Aspect Methods (==) :: TokenBased -> TokenBased -> Bool Source # (/=) :: TokenBased -> TokenBased -> Bool Source #

newtype RangePair Source #

A limited kind of syntax highlighting information: a pair consisting of `Ranges` and `Aspects`.

Note the invariant which `RangePair`s should satisfy (`rangePairInvariant`).

Constructors

RangePair |

Fields

- rangePair :: (Ranges, Aspects)

#### Instances

Instances details

NFData RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: RangePair -> () Source #
Show RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> RangePair -> ShowS Source # show :: RangePair -> String Source # showList :: [RangePair] -> ShowS Source #
IsBasicRangeMap Aspects RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Convert (DelayedMerge RangePair) PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

rangePairInvariant :: RangePair -> Bool Source #

Invariant for `RangePair`.

newtype PositionMap Source #

Syntax highlighting information, represented by maps from positions to `Aspects`.

The first position in the file has number 1.

Constructors

PositionMap |

Fields

- positionMap :: IntMap Aspects

#### Instances

Instances details

NFData PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: PositionMap -> () Source #
Monoid PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: PositionMap Source # mappend :: PositionMap -> PositionMap -> PositionMap Source # mconcat :: [PositionMap] -> PositionMap Source #
Semigroup PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: PositionMap -> PositionMap -> PositionMap Source # sconcat :: NonEmpty PositionMap -> PositionMap Source # stimes :: Integral b => b -> PositionMap -> PositionMap Source #
Show PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> PositionMap -> ShowS Source # show :: PositionMap -> String Source # showList :: [PositionMap] -> ShowS Source #
IsBasicRangeMap Aspects PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
Convert PositionMap (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
Convert (DelayedMerge RangePair) PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #

newtype DelayedMerge hl Source #

Highlighting info with delayed merging.

Merging large sets of highlighting info repeatedly might be costly. The idea of this type is to accumulate small pieces of highlighting information, and then to merge them all at the end.

Note the invariant which values of this type should satisfy (`delayedMergeInvariant`).

Constructors

DelayedMerge (Endo [hl]) |

#### Instances

Instances details

IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
Monoid (DelayedMerge hl) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods mempty :: DelayedMerge hl Source # mappend :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl Source # mconcat :: [DelayedMerge hl] -> DelayedMerge hl Source #
Semigroup (DelayedMerge hl) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DelayedMerge hl -> DelayedMerge hl -> DelayedMerge hl Source # sconcat :: NonEmpty (DelayedMerge hl) -> DelayedMerge hl Source # stimes :: Integral b => b -> DelayedMerge hl -> DelayedMerge hl Source #
Show hl => Show (DelayedMerge hl) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> DelayedMerge hl -> ShowS Source # show :: DelayedMerge hl -> String Source # showList :: [DelayedMerge hl] -> ShowS Source #
Convert (DelayedMerge RangePair) PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Monoid hl => Convert (DelayedMerge hl) hl Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #

delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool Source #

Invariant for ``DelayedMerge` hl`, parametrised by the invariant for `hl`.

Additionally the endofunction should be extensionally equal to `(fs `++`)` for some list `fs`.

type HighlightingInfo = RangeMap Aspects Source #

Highlighting information.

Note the invariant which values of this type should satisfy (`highlightingInfoInvariant`).

This is a type synonym in order to make it easy to change to another representation.

highlightingInfoInvariant :: HighlightingInfo -> Bool Source #

The invariant for `HighlightingInfo`.

type HighlightingInfoBuilder = DelayedMerge RangePair Source #

A type that is intended to be used when constructing highlighting information.

Note the invariant which values of this type should satisfy (`highlightingInfoBuilderInvariant`).

This is a type synonym in order to make it easy to change to another representation.

The type should be an instance of ``IsBasicRangeMap` `Aspects``, `Semigroup` and `Monoid`, and there should be an instance of ``Convert` `HighlightingInfoBuilder` `HighlightingInfo``.

highlightingInfoBuilderInvariant :: HighlightingInfoBuilder -> Bool Source #

The invariant for `HighlightingInfoBuilder`.

Additionally the endofunction should be extensionally equal to `(fs `++`)` for some list `fs`.

## Operations

parserBased :: Aspects Source #

A variant of `mempty` with `tokenBased` set to `NotOnlyTokenBased`.

kindOfNameToNameKind :: KindOfName -> NameKind Source #

Conversion from classification of the scope checker.

class IsBasicRangeMap a m | m -> a where Source #

A class that is intended to make it easy to swap between different range map implementations.

Note that some `RangeMap` operations are not included in this class.

Minimal complete definition

singleton, toMap, toList

Methods

singleton :: Ranges -> a -> m Source #

The map ``singleton` rs x` contains the ranges from `rs`, and every position in those ranges is associated with `x`.

toMap :: m -> IntMap a Source #

Converts range maps to `IntMap`s from positions to values.

toList :: m -> [(Range, a)] Source #

Converts the map to a list. The ranges are non-overlapping and non-empty, and earlier ranges precede later ones in the list.

coveringRange :: m -> Maybe Range Source #

Returns the smallest range covering everything in the map (or `Nothing`, if the range would be empty).

Note that the default implementation of this operation might be inefficient.

#### Instances

Instances details

IsBasicRangeMap Aspects PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> PositionMap Source # toMap :: PositionMap -> IntMap Aspects Source # toList :: PositionMap -> [(Range, Aspects)] Source # coveringRange :: PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects RangePair Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> RangePair Source # toMap :: RangePair -> IntMap Aspects Source # toList :: RangePair -> [(Range, Aspects)] Source # coveringRange :: RangePair -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge PositionMap) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge PositionMap Source # toMap :: DelayedMerge PositionMap -> IntMap Aspects Source # toList :: DelayedMerge PositionMap -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge PositionMap -> Maybe Range Source #
IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> Aspects -> DelayedMerge RangePair Source # toMap :: DelayedMerge RangePair -> IntMap Aspects Source # toList :: DelayedMerge RangePair -> [(Range, Aspects)] Source # coveringRange :: DelayedMerge RangePair -> Maybe Range Source #
Semigroup a => IsBasicRangeMap a (DelayedMerge (RangeMap a)) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods singleton :: Ranges -> a -> DelayedMerge (RangeMap a) Source # toMap :: DelayedMerge (RangeMap a) -> IntMap a Source # toList :: DelayedMerge (RangeMap a) -> [(Range, a)] Source # coveringRange :: DelayedMerge (RangeMap a) -> Maybe Range Source #
IsBasicRangeMap a (RangeMap a) Source # |
Instance details Defined in Agda.Utils.RangeMap Methods singleton :: Ranges -> a -> RangeMap a Source # toMap :: RangeMap a -> IntMap a Source # toList :: RangeMap a -> [(Range, a)] Source # coveringRange :: RangeMap a -> Maybe Range Source #

several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl Source #

Like `singleton`, but with several `Ranges` instead of only one.

class Convert a b where Source #

Conversion between different types.

Methods

convert :: a -> b Source #

#### Instances

Instances details

Convert PositionMap (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) PositionMap Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> PositionMap Source #
Monoid hl => Convert (DelayedMerge hl) hl Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source #
Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source #
Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge RangePair -> RangeMap Aspects Source #
Convert (RangeMap Aspects) (RangeMap Aspects) Source # |
Instance details Defined in Agda.Interaction.Highlighting.Precise Methods convert :: RangeMap Aspects -> RangeMap Aspects Source #

insideAndOutside :: Range -> RangeMap a -> (RangeMap a, RangeMap a) Source #

Returns a `RangeMap` overlapping the given range, as well as the rest of the map.

restrictTo :: Range -> RangeMap a -> RangeMap a Source #

Restricts the `RangeMap` to the given range.

# Orphan instances

NFData Aspect Source # |
Instance details Methods rnf :: Aspect -> () Source #
NFData Aspects Source # |
Instance details Methods rnf :: Aspects -> () Source #
NFData DefinitionSite Source # |
Instance details Methods rnf :: DefinitionSite -> () Source #
NFData OtherAspect Source # |
Instance details Methods rnf :: OtherAspect -> () Source #
Monoid Aspects Source # |
Instance details Methods mempty :: Aspects Source # mappend :: Aspects -> Aspects -> Aspects Source # mconcat :: [Aspects] -> Aspects Source #
Monoid TokenBased Source # |
Instance details Methods mempty :: TokenBased Source # mappend :: TokenBased -> TokenBased -> TokenBased Source # mconcat :: [TokenBased] -> TokenBased Source #
Semigroup Aspects Source # |
Instance details Methods (<>) :: Aspects -> Aspects -> Aspects Source # sconcat :: NonEmpty Aspects -> Aspects Source # stimes :: Integral b => b -> Aspects -> Aspects Source #
Semigroup DefinitionSite Source # |
Instance details Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite Source # sconcat :: NonEmpty DefinitionSite -> DefinitionSite Source # stimes :: Integral b => b -> DefinitionSite -> DefinitionSite Source #
Semigroup TokenBased Source # |
Instance details Methods (<>) :: TokenBased -> TokenBased -> TokenBased Source # sconcat :: NonEmpty TokenBased -> TokenBased Source # stimes :: Integral b => b -> TokenBased -> TokenBased Source #