-
Notifications
You must be signed in to change notification settings - Fork 71
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
Bad syntax highlighting of .lidr files #506
Comments
This used to work!
I suspect a bug in Idris itself, where it's likely sending the source
locations after post processing to get rid of the tracks.
I'm away from the computer on parental leave, but if someone wants to work
on this, check the highlight commands being sent by Idris.
…On Sun, Dec 29, 2019, 06:43 nicolabotta ***@***.***> wrote:
Syntax highlighting works fine on .idr files but on .lidr files (Bird
style), I get something like this:
[image: Screenshot_2019-12-29_15-31-02]
<https://user-images.githubusercontent.com/2726946/71558235-1918e180-2a51-11ea-8ec2-35e321f1b3c1.png>
Is there a way to get the same highlighting on .idr files and .lidr files?
Thanks + cheers, Nicola
—
You are receiving this because you are subscribed to this thread.
Reply to this email directly, view it on GitHub
<#506?email_source=notifications&email_token=AAA4FAQIQ3KTP7PCVTHA36LQ3CZSDA5CNFSM4KA5MGXKYY3PNVWWK3TUL52HS4DFUVEXG43VMWVGG33NNVSW45C7NFSM4IDEA7LQ>,
or unsubscribe
<https://github.com/notifications/unsubscribe-auth/AAA4FAUO7MBMQEU3T4MQRT3Q3CZSDANCNFSM4KA5MGXA>
.
|
Thanks David, I have opened idris-lang/Idris-dev#4799 (comment). Best, Nicola |
As reported in idris-lang/Idris-dev#4799 (comment), there seem to be two problems in the current idris-mode. For syntax highlighting to work as expected for .lidr files, the function
had to be modified as suggested by andrewmcveigh in #480 as
and loaded. The second problem is that the file that defines |
Syntax highlighting works fine on .idr files but on .lidr files (Bird style), I get something like this:
Is there a way to get the same highlighting on .idr files and .lidr files? Thanks + cheers, Nicola
The text was updated successfully, but these errors were encountered: