| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Agda.Interaction.Highlighting.Precise
Description
Types used for precise syntax highlighting.
Synopsis
- data Aspect
- data NameKind
- data OtherAspect
- data Aspects = Aspects {
- aspect :: Maybe Aspect
- otherAspects :: Set OtherAspect
- note :: String
- definitionSite :: Maybe DefinitionSite
- tokenBased :: !TokenBased
- data DefinitionSite = DefinitionSite {
- defSiteModule :: TopLevelModuleName
- defSitePos :: Int
- defSiteHere :: Bool
- defSiteAnchor :: Maybe String
- data TokenBased
- newtype RangePair = RangePair {}
- 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
- 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
Syntactic aspects of the code. (These cannot overlap.)
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
| Eq Aspect Source # | |
| Show Aspect Source # | |
| Generic Aspect Source # | |
| Semigroup Aspect Source # |
|
| NFData Aspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| EmbPrj Aspect Source # | |
| type Rep Aspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise type Rep Aspect = D1 ('MetaData "Aspect" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2-2fIO0qzLA6fLZRIj4yF8z4" '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))))) | |
NameKinds 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
| Eq NameKind Source # | |
| Show NameKind Source # | |
| Generic NameKind Source # | |
| Semigroup NameKind Source # | Some |
| NFData NameKind Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| EmbPrj NameKind Source # | |
| type Rep NameKind Source # | |
Defined in Agda.Interaction.Highlighting.Precise type Rep NameKind = D1 ('MetaData "NameKind" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2-2fIO0qzLA6fLZRIj4yF8z4" '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 Aspects.)
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 |
| TypeChecks | Code which is being type-checked. |
| MissingDefinition | Function declaration without matching definition NB: We put CatchallClause last so that it is overwritten by other, more important, aspects in the emacs mode. |
| CatchallClause | |
| ConfluenceProblem |
Instances
| Bounded OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Enum OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods succ :: OtherAspect -> OtherAspect pred :: OtherAspect -> OtherAspect toEnum :: Int -> OtherAspect fromEnum :: OtherAspect -> Int enumFrom :: OtherAspect -> [OtherAspect] enumFromThen :: OtherAspect -> OtherAspect -> [OtherAspect] enumFromTo :: OtherAspect -> OtherAspect -> [OtherAspect] enumFromThenTo :: OtherAspect -> OtherAspect -> OtherAspect -> [OtherAspect] | |
| Eq OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Ord OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods compare :: OtherAspect -> OtherAspect -> Ordering (<) :: OtherAspect -> OtherAspect -> Bool (<=) :: OtherAspect -> OtherAspect -> Bool (>) :: OtherAspect -> OtherAspect -> Bool (>=) :: OtherAspect -> OtherAspect -> Bool max :: OtherAspect -> OtherAspect -> OtherAspect min :: OtherAspect -> OtherAspect -> OtherAspect | |
| Show OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> OtherAspect -> ShowS show :: OtherAspect -> String showList :: [OtherAspect] -> ShowS | |
| Generic OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise Associated Types type Rep OtherAspect :: Type -> Type | |
| NFData OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: OtherAspect -> () | |
| EmbPrj OtherAspect Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: OtherAspect -> S Int32 Source # icod_ :: OtherAspect -> S Int32 Source # value :: Int32 -> R OtherAspect Source # | |
| type Rep OtherAspect Source # | |
Defined in Agda.Interaction.Highlighting.Precise type Rep OtherAspect = D1 ('MetaData "OtherAspect" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2-2fIO0qzLA6fLZRIj4yF8z4" '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 "CatchallClause" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConfluenceProblem" 'PrefixI 'False) (U1 :: Type -> Type))))) | |
Meta information which can be associated with a character/character range.
Constructors
| Aspects | |
Fields
| |
Instances
data DefinitionSite Source #
Constructors
| DefinitionSite | |
Fields
| |
Instances
| Eq DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods (==) :: DefinitionSite -> DefinitionSite -> Bool (/=) :: DefinitionSite -> DefinitionSite -> Bool | |
| Show DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods showsPrec :: Int -> DefinitionSite -> ShowS show :: DefinitionSite -> String showList :: [DefinitionSite] -> ShowS | |
| Generic DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise Associated Types type Rep DefinitionSite :: Type -> Type | |
| Semigroup DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods (<>) :: DefinitionSite -> DefinitionSite -> DefinitionSite # sconcat :: NonEmpty DefinitionSite -> DefinitionSite stimes :: Integral b => b -> DefinitionSite -> DefinitionSite | |
| NFData DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods rnf :: DefinitionSite -> () | |
| EmbPrj DefinitionSite Source # | |
Defined in Agda.TypeChecking.Serialise.Instances.Highlighting Methods icode :: DefinitionSite -> S Int32 Source # icod_ :: DefinitionSite -> S Int32 Source # value :: Int32 -> R DefinitionSite Source # | |
| type Rep DefinitionSite Source # | |
Defined in Agda.Interaction.Highlighting.Precise type Rep DefinitionSite = D1 ('MetaData "DefinitionSite" "Agda.Interaction.Highlighting.Precise" "Agda-2.6.2-2fIO0qzLA6fLZRIj4yF8z4" 'False) (C1 ('MetaCons "DefinitionSite" 'PrefixI 'True) ((S1 ('MetaSel ('Just "defSiteModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 TopLevelModuleName) :*: 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
A limited kind of syntax highlighting information: a pair
consisting of Ranges and Aspects.
Note the invariant which RangePairs should satisfy
(rangePairInvariant).
Instances
| Show RangePair Source # | |
| NFData RangePair Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| IsBasicRangeMap Aspects RangePair Source # | |
| IsBasicRangeMap Aspects (DelayedMerge RangePair) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
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
| |
Instances
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
delayedMergeInvariant :: (hl -> Bool) -> DelayedMerge hl -> Bool Source #
Invariant for , parametrised by the invariant
for DelayedMerge hlhl.
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 AspectsSemigroup 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.
Methods
singleton :: Ranges -> a -> m Source #
The map contains the ranges from singleton rs xrs, and
every position in those ranges is associated with x.
toMap :: m -> IntMap a Source #
Converts range maps to IntMaps 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
several :: (IsBasicRangeMap a hl, Monoid hl) => [Ranges] -> a -> hl Source #
class Convert a b where Source #
Conversion between different types.
Instances
| Convert PositionMap (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |
| Monoid hl => Convert (DelayedMerge hl) hl Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge hl -> hl Source # | |
| Convert (DelayedMerge RangePair) PositionMap Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods | |
| Convert (RangeMap Aspects) (RangeMap Aspects) Source # | |
| Convert (DelayedMerge PositionMap) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise Methods convert :: DelayedMerge PositionMap -> RangeMap Aspects Source # | |
| Convert (DelayedMerge RangePair) (RangeMap Aspects) Source # | |
Defined in Agda.Interaction.Highlighting.Precise | |