-
Notifications
You must be signed in to change notification settings - Fork 364
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Lexical error with tab character in literate Agda text #5581
Comments
Phil @wadler, would you attach a file with MWE? I cannot reproduce this, tabs in comments seem ok. |
@andreasabel, try putting the following text into
Result:
|
The problem is that literate stuff in a agda/src/full/Agda/Syntax/Parser/Literate.hs Lines 124 to 136 in 78ea6d2
A fix would be to replace tabs by single spaces, that would preserve the character position. |
Implemented this in #5582. |
Agda reports a lexical error when there is a tab in the source code, even if the tab appears in a commented-out part of the source.
The text was updated successfully, but these errors were encountered: