Coq-reST comment parsing fails with parenthetical emphasis in the Alectryon minor-mode

[jhaag]

When I'm using the Alectryon minor mode and in the Coq-view, parsing fails if I have emphasized text at the beginning or the end of a parenthetical, like the following:

(*|

This (**doesn't** work) properly

Neither (does **this**)

(But **this** does)

|*)

[cpitclaudel]

Can you clarify what you mean by parsing fails?

[jhaag]

Basically, if I had a .v file open in Alectryon mode which contained a Coq-reST comment like (*foo* bar ...) or (... foo *bar*), I would get an error message in my message bar saying that Alectryon expected a comment delimiter and it would prevent me from using C-c C-S-a to swap views.

Unfortunately I can't provide more details because the recent update of Alectryon seems to have resolved this; from a .v file, the above forms are allowed and I am able to switch views, and if I swap back to the coq view from the reST view, it inserts backslashes to escape the spaces directly before and after the parentheses. I'm going to close this for now and re-open the issue if I run into it again.

[cpitclaudel]

I think this might be it: this will break:

(*|
This (**doesn't** work) properly
|*)

This is expected, because this code contains an unterminated comment:

(*| ← comment opener
This (** ← comment opener
|*) ← one comment closed
← second comment not closed

I disucss this in the Alectryon blog post on the section about line comments, which solve this problem but aren't available in Coq. The fix is this:

(*|
This (\ **does** work) properly
|*)

(and indeed if you translate a reST file to Coq you'll get the escaping done automatically (and removed when you go back to reST)