ilyakooo0/Idris-dev
1
0
Fork 0
mirror of https://github.com/ilyakooo0/Idris-dev.git synced 2024-09-22 06:29:37 +03:00
Code Issues Projects Releases Wiki Activity

Prevent "(%runTactics foo)" from being an operator

Browse Source 
Previously it was parsed as the application of an unknown operator (%)
in a section.
This commit is contained in:
David Raymond Christiansen 2015-03-02 16:57:28 +01:00
parent e9ff42dc1b
commit 7c1dc9808e
1 changed files with 1 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/Idris/ParseHelpers.hs
View File

@ -326,7 +326,7 @@ commentMarkers :: [String]
commentMarkers = [ "--", "|||" ]
invalidOperators :: [String]
invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]
invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]
-- | Parses an operator
operator :: MonadicParsing m => m String