module Skylighting.Syntax.Idris (syntax) where
import Skylighting.Types
import Data.Map
import Skylighting.Regex
import qualified Data.Set
syntax :: Syntax
syntax = Syntax
{ sName = "Idris"
, sFilename = "idris.xml"
, sShortname = "Idris"
, sContexts =
fromList
[ ( "block comment"
, Context
{ cName = "block comment"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher = Detect2Chars '-' '}'
, rAttribute = CommentTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Pop ]
}
, Rule
{ rMatcher = Detect2Chars '{' '-'
, rAttribute = CommentTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "block comment" ) ]
}
]
, cAttribute = CommentTok
, cLineEmptyContext = []
, cLineEndContext = []
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "char"
, Context
{ cName = "char"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\\\."
, reCompiled = Just (compileRegex True "\\\\.")
, reCaseSensitive = True
}
, rAttribute = CharTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher = DetectChar '\''
, rAttribute = CharTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Pop ]
}
]
, cAttribute = CharTok
, cLineEmptyContext = []
, cLineEndContext = [ Pop ]
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "code"
, Context
{ cName = "code"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher =
RegExpr
RE
{ reString = "---*[^!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?"
, reCompiled =
Just
(compileRegex True "---*[^!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?")
, reCaseSensitive = True
}
, rAttribute = CommentTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "line comment" ) ]
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\|\\|\\|[^\\-!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?"
, reCompiled =
Just
(compileRegex
True "\\|\\|\\|[^\\-!#\\$%&\\*\\+/<=>\\?\\@\\^\\|~\\.:]?")
, reCaseSensitive = True
}
, rAttribute = CommentTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "line comment" ) ]
}
, Rule
{ rMatcher = Detect2Chars '{' '-'
, rAttribute = CommentTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "block comment" ) ]
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString =
"\\s*([a-z]+\\s+)*([A-Za-z][A-Za-z0-9_]*'*|\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\))\\s*:"
, reCompiled =
Just
(compileRegex
True
"\\s*([a-z]+\\s+)*([A-Za-z][A-Za-z0-9_]*'*|\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\))\\s*:")
, reCaseSensitive = True
}
, rAttribute = NormalTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = True
, rFirstNonspace = False
, rColumn = Just 0
, rContextSwitch = [ Push ( "Idris" , "declaration" ) ]
}
, Rule
{ rMatcher =
Keyword
KeywordAttr
{ keywordCaseSensitive = True
, keywordDelims =
Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
}
(makeWordSet
True
[ "abstract"
, "auto"
, "case"
, "class"
, "codata"
, "covering"
, "data"
, "default"
, "do"
, "dsl"
, "else"
, "if"
, "implicit"
, "import"
, "impossible"
, "in"
, "index_first"
, "index_next"
, "infix"
, "infixl"
, "infixr"
, "instance"
, "lambda"
, "let"
, "module"
, "mututal"
, "namespace"
, "of"
, "parameters"
, "partial"
, "pattern"
, "postulate"
, "prefix"
, "private"
, "proof"
, "public"
, "record"
, "rewrite"
, "static"
, "syntax"
, "tactics"
, "term"
, "then"
, "total"
, "using"
, "variable"
, "where"
, "with"
])
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher = DetectChar '%'
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "directive" ) ]
}
, Rule
{ rMatcher =
Keyword
KeywordAttr
{ keywordCaseSensitive = True
, keywordDelims =
Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
}
(makeWordSet
True
[ "applyTactic"
, "attack"
, "compute"
, "exact"
, "fill"
, "focus"
, "induction"
, "intro"
, "intros"
, "let"
, "refine"
, "reflect"
, "rewrite"
, "solve"
, "trivial"
, "try"
])
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher = DetectChar '\''
, rAttribute = CharTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "char" ) ]
}
, Rule
{ rMatcher = DetectChar '"'
, rAttribute = StringTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Push ( "Idris" , "string" ) ]
}
, Rule
{ rMatcher = Int
, rAttribute = DecValTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "0[Xx][0-9A-Fa-f]+"
, reCompiled = Just (compileRegex True "0[Xx][0-9A-Fa-f]+")
, reCaseSensitive = True
}
, rAttribute = BaseNTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "0[Xx][0-9A-Fa-f]+"
, reCompiled = Just (compileRegex True "0[Xx][0-9A-Fa-f]+")
, reCaseSensitive = True
}
, rAttribute = BaseNTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\d+\\.\\d+([eE][-+]?\\d+)?"
, reCompiled =
Just (compileRegex True "\\d+\\.\\d+([eE][-+]?\\d+)?")
, reCaseSensitive = True
}
, rAttribute = FloatTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "([A-Z][a-zA-Z0-9_]*'*|_\\|_)"
, reCompiled =
Just (compileRegex True "([A-Z][a-zA-Z0-9_]*'*|_\\|_)")
, reCaseSensitive = True
}
, rAttribute = DataTypeTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "[a-z][a-zA-Z0-9_]*'*"
, reCompiled = Just (compileRegex True "[a-z][a-zA-Z0-9_]*'*")
, reCaseSensitive = True
}
, rAttribute = NormalTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\?[a-z][A-Za-z0-9_]+'*"
, reCompiled = Just (compileRegex True "\\?[a-z][A-Za-z0-9_]+'*")
, reCaseSensitive = True
}
, rAttribute = OtherTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "(:|=>|\\->|<\\-)"
, reCompiled = Just (compileRegex True "(:|=>|\\->|<\\-)")
, reCaseSensitive = True
}
, rAttribute = OtherTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+|\\b_\\b)"
, reCompiled =
Just
(compileRegex
True "([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+|\\b_\\b)")
, reCaseSensitive = True
}
, rAttribute = FunctionTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "`[A-Za-z][A-Za-z0-9_]*'*`"
, reCompiled = Just (compileRegex True "`[A-Za-z][A-Za-z0-9_]*'*`")
, reCaseSensitive = True
}
, rAttribute = FunctionTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
]
, cAttribute = NormalTok
, cLineEmptyContext = []
, cLineEndContext = []
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "declaration"
, Context
{ cName = "declaration"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher =
Keyword
KeywordAttr
{ keywordCaseSensitive = True
, keywordDelims =
Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
}
(makeWordSet
True
[ "abstract"
, "auto"
, "case"
, "class"
, "codata"
, "covering"
, "data"
, "default"
, "do"
, "dsl"
, "else"
, "if"
, "implicit"
, "import"
, "impossible"
, "in"
, "index_first"
, "index_next"
, "infix"
, "infixl"
, "infixr"
, "instance"
, "lambda"
, "let"
, "module"
, "mututal"
, "namespace"
, "of"
, "parameters"
, "partial"
, "pattern"
, "postulate"
, "prefix"
, "private"
, "proof"
, "public"
, "record"
, "rewrite"
, "static"
, "syntax"
, "tactics"
, "term"
, "then"
, "total"
, "using"
, "variable"
, "where"
, "with"
])
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "([A-Z][a-zA-Z0-9_]*'*|_\\|_)"
, reCompiled =
Just (compileRegex True "([A-Z][a-zA-Z0-9_]*'*|_\\|_)")
, reCaseSensitive = True
}
, rAttribute = DataTypeTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "[a-z][A-Za-z0-9_]*'*"
, reCompiled = Just (compileRegex True "[a-z][A-Za-z0-9_]*'*")
, reCaseSensitive = True
}
, rAttribute = FunctionTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\)"
, reCompiled =
Just
(compileRegex
True "\\([\\-!#\\$%&\\*\\+\\./<=>\\?@\\\\^\\|~:]+\\)")
, reCaseSensitive = True
}
, rAttribute = FunctionTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher = DetectChar ':'
, rAttribute = OtherTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Pop ]
}
]
, cAttribute = NormalTok
, cLineEmptyContext = []
, cLineEndContext = [ Pop ]
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "directive"
, Context
{ cName = "directive"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher =
Keyword
KeywordAttr
{ keywordCaseSensitive = True
, keywordDelims =
Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
}
(makeWordSet
True
[ "abstract"
, "auto"
, "case"
, "class"
, "codata"
, "covering"
, "data"
, "default"
, "do"
, "dsl"
, "else"
, "if"
, "implicit"
, "import"
, "impossible"
, "in"
, "index_first"
, "index_next"
, "infix"
, "infixl"
, "infixr"
, "instance"
, "lambda"
, "let"
, "module"
, "mututal"
, "namespace"
, "of"
, "parameters"
, "partial"
, "pattern"
, "postulate"
, "prefix"
, "private"
, "proof"
, "public"
, "record"
, "rewrite"
, "static"
, "syntax"
, "tactics"
, "term"
, "then"
, "total"
, "using"
, "variable"
, "where"
, "with"
])
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
Keyword
KeywordAttr
{ keywordCaseSensitive = True
, keywordDelims =
Data.Set.fromList "\t\n !%&()*+,-./:;<=>?[\\]^{|}~"
}
(makeWordSet
True
[ "access"
, "assert_total"
, "default"
, "dynamic"
, "elim"
, "error_handlers"
, "error_reverse"
, "flag"
, "hide"
, "include"
, "language"
, "lib"
, "link"
, "name"
, "provide"
, "reflection"
])
, rAttribute = KeywordTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
]
, cAttribute = NormalTok
, cLineEmptyContext = []
, cLineEndContext = [ Pop ]
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "line comment"
, Context
{ cName = "line comment"
, cSyntax = "Idris"
, cRules = []
, cAttribute = CommentTok
, cLineEmptyContext = []
, cLineEndContext = [ Pop ]
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
, ( "string"
, Context
{ cName = "string"
, cSyntax = "Idris"
, cRules =
[ Rule
{ rMatcher =
RegExpr
RE
{ reString = "\\\\."
, reCompiled = Just (compileRegex True "\\\\.")
, reCaseSensitive = True
}
, rAttribute = StringTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = []
}
, Rule
{ rMatcher =
RegExpr
RE
{ reString = "\""
, reCompiled = Just (compileRegex True "\"")
, reCaseSensitive = True
}
, rAttribute = StringTok
, rIncludeAttribute = False
, rDynamic = False
, rCaseSensitive = True
, rChildren = []
, rLookahead = False
, rFirstNonspace = False
, rColumn = Nothing
, rContextSwitch = [ Pop ]
}
]
, cAttribute = StringTok
, cLineEmptyContext = []
, cLineEndContext = []
, cLineBeginContext = []
, cFallthrough = False
, cFallthroughContext = []
, cDynamic = False
}
)
]
, sAuthor = "Alexander Shabalin"
, sVersion = "1.0"
, sLicense = "LGPL"
, sExtensions = [ "*.idr" ]
, sStartingContext = "code"
}