The errors are incorrectly located

[mrakgr]

I am guessing the plugin is incorrectly counting lines for some reason. In the attached screenshot it literally puts me 15 lines away from the error every time I compile. It is quite distracting.

I also find it annoying that every time I compile I need to save manually beforehand. I've also ran into issues when compiling would not clear the buffer and it would show me the old goal in the same place though that might be just me forgetting to save.

I am using Atom on Windows 10.

[mrakgr]

I forgot to mention, the same goes for highlighting of the errors.

[banacorn]

Does this incorrect line-counting also happens on .agda files, or just .lagda files?

I'll see why save-before-load is not working.

[mrakgr]

It happens for both.

[banacorn]

I've been writing tests recently (finally) and found some glitches in parsing highlighting locations!

[DimaSamoz]

Not sure if this is still active, but I've been having similar issues: the highlighting showing the warning or error has the correct "shape" but is shifted. Attached is an example: the first line is what compilation displays, the second line is the same text but shifted by 10 spaces to the left to show how the text should be aligned with the highlighting.

Thank you for your work on Agda support in Atom!

[banacorn]

@DimaSamoz thank you for reporting this. Could you provide a piece of code that causes this problem?

[DimaSamoz]

Hmm not sure how minimal of an example I can find, since the issue usually arises for larger files... I'll try to put something together when I have time!