Table of contents styling

[JasonGross]

I think the table of contents is ugly. We should pick a better styling for chapter/file headings.

[mikeshulman]

I think Coqdoc's output is fairly ugly in any case, but yes, it would be nice to have better conventions about headings. It's unfortunate that the only way to give a "title" to an entire file is to use a top-level heading (** * ... *) which then translates into a lonely top-level bullet point in the output.

[JasonGross]

We could use --lib-subtitles and (** * ModuleName : text *), which gives us a "subtitle". I've never tried it, and don't know how it looks.

[spitters]

Yann is working on an improved coqdoc-ng, but I don't know how much is already in trunk.

On Mon, Oct 13, 2014 at 6:53 AM, Jason Gross [email protected] wrote:

We could use --lib-subtitles and (** * ModuleName : text *) http://coq.inria.fr/refman/Reference-Manual017.html#sec597, which gives us a "subtitle". I've never tried it, and don't know how it looks.

— Reply to this email directly or view it on GitHub https://github.com/HoTT/HoTT/issues/570#issuecomment-58845005.

[andrejbauer]

Obviously they should produce vanilla HTML and use CSS for the looks. I remember being annoyed by coqdoc in the past for being so outdated.

[JasonGross]

@andrejbauer, I think that is already what happens, at least in trunk. At the very least, inspecting the html of the toc shows plain html, with the styling being done by coqdoc.css.

[andrejbauer]

well them we just need to hack the CSS