7c1dc98 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

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

Previously it was parsed as the application of an unknown operator (%) in a section.

commit7c1dc9808ead86873d9b032c0419a2cd24a8215f authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 2 Mar 2015, 16:57 (12 years ago) parente9ff42d

1 file changed+1−1

compare with master

unifiedsplit

src/Idris/ParseHelpers.hs+1−1

src/Idris/ParseHelpers.hs+1−1

@@ -326,7 +326,7 @@ commentMarkers :: [String]

326326commentMarkers = [ "--", "|||" ]

327327

328328invalidOperators :: [String]

329−invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\"]

329+invalidOperators = [":", "=>", "->", "<-", "=", "?=", "|", "**", "==>", "\\", "%"]

330330

331331-- | Parses an operator