Misaligned Literate Idris highlightling in idris-mode

[fabianhjr]

> data Day = Monday
>          | Tuesday
>          | Wednesday
>          | Thursday
>          | Friday
>          | Saturday
>          | Sunday
>
> next_weekday : Day -> Day
> next_weekday d = case d of
>                      Monday    => Tuesday
>                      Tuesday   => Wednesday
>                      Wednesday => Thursday
>                      Thursday  => Friday
>                      Friday    => Saturday
>                      Saturday  => Sunday
>                      Sunday    => Monday

Steps to Reproduce

1. Save code as Literate.lidr
2. idris-load-file in Emacs with idris-mode

Expected Behavior

Correct highlighting

Observed Behavior

Highlighting shifts 2 places to the left. (Corresponding to the > in the editor)

Software Info

idris --version: 1.3.0-git:PRE
emacs --version: GNU Emacs 26.1

Related: idris-lang/Idris-dev#1736

Crosspost from idris-lang/Idris-dev#4478

[ska80]

I don't have this issue:

idris --version: 1.3.0-git:88a9f38f
emacs --version: GNU Emacs 26.1

idris-mode: latest, installed from MELPA

[fabianhjr]

Thanks @ska80, I will double check my configs to see if there is something messing with my buffer.

[andrewmcveigh]

I do have this issue, did you solve it?

[andrewmcveigh]

Seems to be down to this 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)))

Changing it to this "fixes" the offset for me.

(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)))

Maybe something in the back end changed for .lidr?

[lrworth]

@fabianhjr @andrewmcveigh I too have this issue. Was there some resolution found before the ticket was closed?

I'm using Spacemacs with the idris layer. I can fix it the same way @andrewmcveigh suggested.

[fabianhjr]

I don't remember how I fixed it but it was an issue on my end.

[jjl]

I just upgraded idris-mode from melpa and see the same problem. evaluating the code by @andrewmcveigh also fixes it.