Idris.IDEMode.TokenLine

Tokenise a source line for easier processing

Definitions

RawName : Type

Totality: total
Visibility: public export

data SourcePart : Type

Totality: total
Visibility: public export
Constructors:

Whitespace : String -> SourcePart

Name : RawName -> SourcePart

HoleName : String -> SourcePart

LBrace : SourcePart

RBrace : SourcePart

Equal : SourcePart

AsPattern : SourcePart

Other : String -> SourcePart

toString : SourcePart -> String

Totality: total
Visibility: export

tokens : String -> List SourcePart

Totality: total
Visibility: export