The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Le 21 févr. 09 à 15:36, Benjamin Pierce a écrit :

> I've been trying to get use coqdoc to make a nice HTML version of my  
> under-construction lecture notes for teaching PL using Coq, but I'm  
> stuck on one serious deficiency: there seems to be no way to get it  
> to keep ordinary comments -- in particular, comments within proofs.   
> I've had a little look inside the code, but I'm afraid I can't  
> understand how it works well enough to see whether this would be  
> easy or hard to change.  Can anyone comment on this?

Hi Benjamin,

I can comment :) coqdoc currently skips comments on purpose, in the  
entry "comment" in file
pretty.mll and it is quite straightforward to make it output the  
contents instead. Here's a
patch that does it, putting comments in a <span id="comment"> if you  
add the --parse-comments
option. Feel free to modify and feed back to me.

-- Matthieu

Attachment: parse_comments.diff
Description: Binary data