@@ -245,20 +245,20 @@ float = do f <- Tok.double
246-- | Idris Style for parsing identifiers/reserved keywords
246-- | Idris Style for parsing identifiers/reserved keywords
247idrisStyle :: MonadicParsing m => IdentifierStyle m
247idrisStyle :: MonadicParsing m => IdentifierStyle m
248−idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved Hi.Identifier Hi.ReservedIdentifier
248+idrisStyle = IdentifierStyle {
249− where _styleName = "Idris"
249+ _styleName = "Idris"
250− _styleStart = satisfy isAlpha <|> oneOf "_"
250+ , _styleStart = satisfy isAlpha <|> oneOf "_"
251− _styleLetter = satisfy isAlphaNum <|> oneOf "_'."
251+ , _styleLetter = satisfy isAlphaNum <|> oneOf "_'."
252+ , _styleReserved = HS.fromList
252− _styleReserved = HS.fromList ["let", "in", "data", "codata", "record", "corecord", "Type",
253+ ["let", "in", "data", "codata", "record", "corecord", "Type", "do", "dsl",
253− "do", "dsl", "import", "impossible",
254− "case", "of", "total", "partial", "mutual",
254+ "import", "impossible", "case", "of", "total", "partial", "mutual",
255− "infix", "infixl", "infixr", "rewrite",
255+ "infix", "infixl", "infixr", "rewrite", "where", "with", "syntax",
256− "where", "with", "syntax", "proof", "postulate",
257− "using", "namespace", "class", "instance",
256+ "proof", "postulate", "using", "namespace", "class", "instance",
258− "interface", "implementation", "parameters",
257+ "interface", "implementation", "parameters", "public", "private",
259− "public", "private", "export", "abstract", "implicit",
260− "quoteGoal", "constructor",
258+ "export", "abstract", "implicit", "quoteGoal", "constructor", "if",
261− "if", "then", "else"]
259+ "then", "else"]
260+ , _styleHighlight = Hi.Identifier
261+ , _styleReservedHighlight = Hi.ReservedIdentifier }
263char :: MonadicParsing m => Char -> m Char
263char :: MonadicParsing m => Char -> m Char
264char = Chr.char
264char = Chr.char
@@ -293,7 +293,7 @@ reserved = Tok.reserve idrisStyle
293-- reserved identifiers never contain line breaks.
293-- reserved identifiers never contain line breaks.
294reservedFC :: MonadicParsing m => String -> m FC
294reservedFC :: MonadicParsing m => String -> m FC
295reservedFC str = do (FC file (l, c) _) <- getFC
295reservedFC str = do (FC file (l, c) _) <- getFC
296− Tok.reserve idrisStyle str
296+ reserved str
297 return $ FC file (l, c) (l, c + length str)
297 return $ FC file (l, c) (l, c + length str)
299-- | Parse a reserved identfier, highlighting its span as a keyword
299-- | Parse a reserved identfier, highlighting its span as a keyword
@@ -308,10 +308,9 @@ reservedOp name = token $ try $
308 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
308 notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
310reservedOpFC :: MonadicParsing m => String -> m FC
310reservedOpFC :: MonadicParsing m => String -> m FC
311−reservedOpFC name = token $ try $ do (FC f (l, c) _) <- getFC
311+reservedOpFC name = do (FC f (l, c) _) <- getFC
312− string name
312+ reservedOp name
313− notFollowedBy (operatorLetter) <?> ("end of " ++ show name)
314− return (FC f (l, c) (l, c + length name))
313+ return (FC f (l, c) (l, c + length name))
316-- | Parses an identifier as a token
315-- | Parses an identifier as a token
317identifier :: (MonadicParsing m) => m (String, FC)
316identifier :: (MonadicParsing m) => m (String, FC)
@@ -393,7 +392,7 @@ commentMarkers :: [String]
393commentMarkers = [ "--", "|||" ]
392commentMarkers = [ "--", "|||" ]
395invalidOperators :: [String]
394invalidOperators :: [String]
396−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!"]
395+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%", "~", "?", "!", "@"]
398-- | Parses an operator
397-- | Parses an operator
399operator :: MonadicParsing m => m String
398operator :: MonadicParsing m => m String
@@ -404,12 +403,9 @@ operator = do op <- token . some $ operatorLetter
405-- | Parses an operator
404-- | Parses an operator
406operatorFC :: MonadicParsing m => m (String, FC)
405operatorFC :: MonadicParsing m => m (String, FC)
407−operatorFC = do (op, fc) <- token $ do (FC f (l, c) _) <- getFC
406+operatorFC = do (FC f (l, c) _) <- getFC
408− op <- some operatorLetter
407+ op <- operator
409− return (op, FC f (l, c) (l, c + length op))
408+ return (op, FC f (l, c) (l, c + length op))
410− when (op `elem` (invalidOperators ++ commentMarkers)) $
411− fail $ op ++ " is not a valid operator"
414{- * Position helpers -}
410{- * Position helpers -}
415{- | Get filename from position (returns "(interactive)" when no source file is given) -}
411{- | Get filename from position (returns "(interactive)" when no source file is given) -}