Feature request: split comments, not just code

[cpitclaudel]

trafficstars

Hi Emilio,

Hope you're doing OK despite the crazy times. In the project I'm workig on, it would be very useful to be able to get comments boundaries in addition to code fragments; like this:

("query0" (Add () "Goal True.\n  (* R1 *)  (** D1 **) idtac. (* R2 *)"))
(Answer query0 Ack)
(Answer query0(Added 2((fname ToplevelInput)(line_nb 1)(bol_pos 0)(line_nb_last 1)(bol_pos_last 0)(bp 0)(ep 10))NewTip))
(Answer query0(Added 3((fname ToplevelInput)(line_nb 2)(bol_pos 11)(line_nb_last 2)(bol_pos_last 11)(bp 34)(ep 40))NewTip))
(Answer query0 Completed)

It would be great if instead of two spans (0-10, 34-40), SerAPI could return 5: Goal True., (* R1 *), (** D1 **), idtac., (* R2 *).

Currently I have a mini-parser that I use after passing things through SerAPI, to detect comment boundaries.

WDYT?

Thanks!

[ejgallego]

Hi Clément, thanks, I hope you folks are doing well too!

This is pretty similar to #191 , and it's been on the table for a while, I just lack the cycles right now as this would involve modifying Coq's parser. I will provide some workaround for 8.12 tho, so at least the Python (client) side can recover comments from files and slice them back.

[ejgallego]

Indeed, what we can provide for now is a wrapper to 8.12's:

    val get_comments : t -> ((int * int) * string) list

[cpitclaudel]

That would be very nice, indeed.

[ejgallego]

That would be very nice, indeed

Still this defers the insertion of comments to the clients which is not ideal, the problem is that Coq doesn't recognize comments as part of the document, so they don't have a statement_id, but if we could do this SerAPI-side it would be great, maybe we could add a call that would output the document decorated somehow.

[ejgallego]

#205 should help with this, will be included in the next release. Still far from what you would like [likely impossible to solve properly unless we introduce #5 first).

For now, I'm not closing but postponing further improvements.

[cpitclaudel]

Thanks a lot, sorry for the long delay in my answer. This looks good. I think your link to #5 is quite relevant too, indeed; for now for that I have a comment parser written in Python.