Improve navigation in API reference.
* src/tools/docmaker/tohtml.py (html_header_3): Renamed to...
(html_header_6): This.
(html_header_3, html_header_3i, html_header_4, html_header_5,
html_header_5t): New strings.
(toc_footer_start, toc_footer_end): New strings.
(HtmlFormatter::html_header): Updated.
(HtmlFormatter::html_index_header, HtmlFormatter::html_toc_header):
New strings.
(HtmlFormatter::index_enter): Use `html_index_header'.
(HtmlFormatter::index_exit): Print `html_footer'.
(HtmlFormatter::toc_enter): Use `html_toc_header'.
(HtmlFormatter::toc_exit): Print proper footer.
Convert ~ to non-breakable space.
* src/tools/docmaker/tohtml.py (make_html_para): Implement it.
Update header files accordingly.
Many other minor documentation fixes.
35 files changed
