Using double quotes ('"') or character sequences for comments ("--" or "{-") in inline documentation severely messes up the highlighting.

[greatBigDot]

I ran into some odd behavior when using Idris' inline documentation features. I first noticed the problem when using double quotes:

||| This is a representation of a "Magma", an algebraic structure with ...
interface Magma ...

In the docs, the quoted word "Magma" (and the surrounding quotation marks) is highlighted in the string font; everything else on the line reverts back to the normal color for the code instead of the documentation style. When I noticed this, I tried removing the closing quote:

||| "testing
test : Integer
test = 42

Sure enough, everything below the documentation gets highlighted in the documentation font. Furthermore, it turns out that the comment starters "{-" and "--" also cause this behavior. The character sequence "{-" will ruin the highlighting beneath it until it hits a matching "-}". (Note that Idris doesn't allow comments inside documentation or anything like that; running idris --mkdoc will result in the "commented" documentation being present in the generated docs, despite idris-mode's highlighting.)

This behavior does not occur within normal comments---only inline documentation behaves like this.

Ironically enough, when enclosed in double quotes, "{-" and "--" don't affect the highlighting; the same goes for the other 5 combinations.

---

As a fix, one can simply escape the troublesome characters with a backslash; idris --mkdoc removes the backslashes in the generated docs, and idris-mode won't try to have them start a new highlighting environment. Without doing this, the faulty highlighting renders the code utterly unreadable whenever documentation contains an unmatched '"' or "{-".

---

This behavior occurs in version 20180416.2245 (the most recent release).

[david-christiansen]

I've noticed this myself - it's an unfortunate limitation of the current highlighting code. Thanks for the report!

[peterb12]

Sadly this makes things look pretty ridiculous in the Idris translation of the Software Foundations text. :-(