Safe Haskell	None
Language	Haskell98

Agda.Interaction.Highlighting.Precise

Contents

Files
- Creation
- Inspection
Compressed files
- Creation
- Inspection
Tests

Description

Types used for precise syntax highlighting.

Synopsis

Files

data Aspect Source #

Syntactic aspects of the code. (These cannot overlap.) They can be obtained from the lexed tokens already, except for the NameKind.

Constructors

Comment
Keyword
String
Number
Symbol	Symbols like forall, =, ->, etc.
PrimitiveType	Things like Set and Prop.
Name (Maybe NameKind) Bool	Is the name an operator part?

Instances

Eq Aspect Source #
Methods (==) :: Aspect -> Aspect -> Bool # (/=) :: Aspect -> Aspect -> Bool #
Show Aspect Source #
Methods showsPrec :: Int -> Aspect -> ShowS # show :: Aspect -> String # showList :: [Aspect] -> ShowS #
Arbitrary Aspect Source #
Methods arbitrary :: Gen Aspect # shrink :: Aspect -> [Aspect] #
CoArbitrary Aspect Source #
Methods coarbitrary :: Aspect -> Gen b -> Gen b #

data NameKind Source #

NameKinds are figured our during scope checking.

Constructors

Bound	Bound variable.
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 #
Methods (==) :: NameKind -> NameKind -> Bool # (/=) :: NameKind -> NameKind -> Bool #
Show NameKind Source #
Methods showsPrec :: Int -> NameKind -> ShowS # show :: NameKind -> String # showList :: [NameKind] -> ShowS #
Arbitrary NameKind Source #
Methods arbitrary :: Gen NameKind # shrink :: NameKind -> [NameKind] #
CoArbitrary NameKind Source #
Methods coarbitrary :: NameKind -> Gen b -> Gen b #

data OtherAspect Source #

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

Constructors

Error
DottedPattern
UnsolvedMeta
UnsolvedConstraint	Unsolved constraint not connected to meta-variable. This could for instance be an emptyness constraint.
TerminationProblem
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.

Instances

Bounded OtherAspect Source #
Methods minBound :: OtherAspect # maxBound :: OtherAspect #
Enum OtherAspect Source #
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 #
Methods (==) :: OtherAspect -> OtherAspect -> Bool # (/=) :: OtherAspect -> OtherAspect -> Bool #
Show OtherAspect Source #
Methods showsPrec :: Int -> OtherAspect -> ShowS # show :: OtherAspect -> String # showList :: [OtherAspect] -> ShowS #
Arbitrary OtherAspect Source #
Methods arbitrary :: Gen OtherAspect # shrink :: OtherAspect -> [OtherAspect] #
CoArbitrary OtherAspect Source #
Methods coarbitrary :: OtherAspect -> Gen b -> Gen b #

data Aspects Source #

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

Constructors

Aspects

Fields

aspect :: Maybe Aspect
otherAspects :: [OtherAspect]
note :: Maybe String
This note, if present, 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 (TopLevelModuleName, Int)
The definition site of the annotated thing, if applicable and known. File positions are counted from 1.

Instances

Eq Aspects Source #
Methods (==) :: Aspects -> Aspects -> Bool # (/=) :: Aspects -> Aspects -> Bool #
Show Aspects Source #
Methods showsPrec :: Int -> Aspects -> ShowS # show :: Aspects -> String # showList :: [Aspects] -> ShowS #
Monoid Aspects Source #
Methods mempty :: Aspects # mappend :: Aspects -> Aspects -> Aspects # mconcat :: [Aspects] -> Aspects #
Arbitrary Aspects Source #
Methods arbitrary :: Gen Aspects # shrink :: Aspects -> [Aspects] #
CoArbitrary Aspects Source #
Methods coarbitrary :: Aspects -> Gen b -> Gen b #

data File Source #

A File is a mapping from file positions to meta information.

The first position in the file has number 1.

Instances

Eq File Source #
Methods (==) :: File -> File -> Bool # (/=) :: File -> File -> Bool #
Show File Source #
Methods showsPrec :: Int -> File -> ShowS # show :: File -> String # showList :: [File] -> ShowS #
Monoid File Source #
Methods mempty :: File # mappend :: File -> File -> File # mconcat :: [File] -> File #
Arbitrary File Source #
Methods arbitrary :: Gen File # shrink :: File -> [File] #
CoArbitrary File Source #
Methods coarbitrary :: File -> Gen b -> Gen b #

type HighlightingInfo = CompressedFile Source #

Syntax highlighting information.

Creation

singleton :: Ranges -> Aspects -> File Source #

singleton rs m is a file whose positions are those in rs, and in which every position is associated with m.

several :: [Ranges] -> Aspects -> File Source #

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

Inspection

smallestPos :: File -> Maybe Int Source #

Returns the smallest position, if any, in the File.

toMap :: File -> IntMap Aspects Source #

Convert the File to a map from file positions (counting from 1) to meta information.

Compressed files

newtype CompressedFile Source #

A compressed File, in which consecutive positions with the same Aspects are stored together.

Constructors

CompressedFile
Fields ranges :: [(Range, Aspects)]

Instances

Eq CompressedFile Source #
Methods (==) :: CompressedFile -> CompressedFile -> Bool # (/=) :: CompressedFile -> CompressedFile -> Bool #
Show CompressedFile Source #
Methods showsPrec :: Int -> CompressedFile -> ShowS # show :: CompressedFile -> String # showList :: [CompressedFile] -> ShowS #
Monoid CompressedFile Source #
Methods mempty :: CompressedFile # mappend :: CompressedFile -> CompressedFile -> CompressedFile # mconcat :: [CompressedFile] -> CompressedFile #
Arbitrary CompressedFile Source #
Methods arbitrary :: Gen CompressedFile # shrink :: CompressedFile -> [CompressedFile] #

compressedFileInvariant :: CompressedFile -> Bool Source #

Invariant for compressed files.

Note that these files are not required to be maximally compressed, because ranges are allowed to be empty, and the Aspectss in adjacent ranges are allowed to be equal.

compress :: File -> CompressedFile Source #

Compresses a file by merging consecutive positions with equal meta information into longer ranges.

decompress :: CompressedFile -> File Source #

Decompresses a compressed file.

noHighlightingInRange :: Ranges -> CompressedFile -> CompressedFile Source #

Clear any highlighting info for the given ranges. Used to make sure unsolved meta highlighting overrides error highlighting.

Creation

singletonC :: Ranges -> Aspects -> CompressedFile Source #

singletonC rs m is a file whose positions are those in rs, and in which every position is associated with m.

severalC :: [Ranges] -> Aspects -> CompressedFile Source #

Like singletonR, but with a list of Ranges instead of a single one.

splitAtC :: Int -> CompressedFile -> (CompressedFile, CompressedFile) Source #

splitAtC p f splits the compressed file f into (f1, f2), where all the positions in f1 are < p, and all the positions in f2 are >= p.

selectC :: Range -> CompressedFile -> CompressedFile Source #

Inspection

smallestPosC :: CompressedFile -> Maybe Int Source #

Returns the smallest position, if any, in the CompressedFile.

Tests

tests :: IO Bool Source #

All the properties.