Javascript-powered per-lemma proof visibility toggling in coqdoc HTML output.

[coqbot]

Note: the issue was created automatically with bugzilla2github tool

Original bug ID: BZ#2201
From: @Eelis
Reported version: unspecified
CC: @pirbo

[coqbot]

Comment author: @Eelis

Currently one can pass -g to coqdoc to hide proofs. For the HTML output, I think we can do better than this "all or nothing" approach. There, it should be possible to add a little button next to each lemma that toggles its proof's visibility (alternatively, the lemma itself could be the "button"). This should require only a modicum of Javascript. As a finishing touch, there could be "hide all" / "show all" buttons at the top of each .html.

[coqbot]

Comment author: @pirbo

Poor Yann, he should have never say that he'll rewrite coqdoc ...
Anyway, one more wish to study !

[daniel-freiermuth]

Does this fulfill your expectations? https://www.ps.uni-saarland.de/~ttebbi/coqdocjs/

[Zimmi48]

Looks like an alternative to proviola. Anyways, I wish people would submit their patches to improve coqdoc instead of making their own extensions.

[anton-trunov]

@Zimmi48 It would be cool if you as a Coq dev encouraged the author(s) here https://github.com/tebbi/coqdocjs/issues

[gares]

@Hc10b why don't you create a PR with your changes? The resulting HTML is pretty nice to me! And the changes seems reasonable (a few extra files).

[Zimmi48]

@gares I don't think @Hc10b was claiming this work was their own. From the link that @anton-trunov gave, it looks like the author is @tebbi.

[daniel-freiermuth]

Right. I have used coqdocjs once and stumbling about this open issue, I just want to leave a hint for people looking for something similar.