Bad syntax highlighting of .lidr files

[nicolabotta]

In idris-mode, syntax highlighting works fine on .idr files but on .lidr files (Bird style), I get something like this:

At idris-hackers/idris-mode#506 (comment),
@david-christiansen suggests that this might be an Idris bug. Any idea how to fix the problem? Thanks, Nicola

[david-christiansen]

In any case, the two disagree about the meaning of source positions!

The first place to check is whether the output from Idris is in fact correct. If not, it's probably source positions in the parser after the delit stage for lidr files. If so, then the Emacs mode probably has an obsolete hack that needs removing - see the highlight buffer on load bit.

[nicolabotta]

David, I am afraid I do not understand any single bit of your comment. I guess this is fine, I am an Idris user, not a developer. I just would like to get a decent syntax highlighting in literate Idris files. This is what I use both for program development and for presentations. Cheers, Nicola

[fabianhjr]

@nicolabotta, I closed #4478 in idris-dev since it was an issue with idris-mode and not the idris compiler/ide interface.

Check in idris-hackers/idris-mode#480 for more help. Apparently I had a configuration issue back then but it could have been a regression in your case.

[nicolabotta]

@fabianhjr: Thanks for your feedback Fabian! There seem to be two problems with the current idris-mode: first, the function

(defun idris-highlight-column (idris-col)
  "Compute the Emacs position offset of the Idris column IDRIS-COL, for highlighting.                                     
                                                                                                                          
In particular, this takes bird tracks into account in literate Idris."
  (+ idris-col (if (idris-lidr-p) 1 -1)))

needs to be modified as suggested by andrewmcveigh in idris-hackers/idris-mode#480 as

(defun idris-highlight-column (idris-col)
  "Compute the Emacs position offset of the Idris column IDRIS-COL, for highlighting.                                     
                                                                                                                          
In particular, this takes bird tracks into account in literate Idris."
  (+ idris-col (if (idris-lidr-p) -1 -1)))

Second, the file in which this function is defined, idris-highlight-input.el, needs to be manually loaded. When idris-mode is loaded, this file is not loaded, for some reason.