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