toc toggle button

The TOC toggle button was very small and inconspicuous. This patch
replaces the old one with small arrows placed at the right border
of the TOC header.
Code cleanup in html.php: html_toc() and html_list_toc() are obsolete
and have been removed.

darcs-hash:20050531184155-7ef76-249f948b2a8b71d45aab2b8418db2be5eb638f6d.gz