doc: Generate, embed and animate a table of contents in the navbar itself
authorRamprasad Venkataraman <ramv@illinois.edu>
Mon, 6 Aug 2012 22:50:32 +0000 (17:50 -0500)
committerRamprasad Venkataraman <ramv@illinois.edu>
Tue, 7 Aug 2012 04:34:20 +0000 (23:34 -0500)
commit729a3bf6fb708b097f89790d561ed9f3f5067f21
tree0164470e8ceaa596d2668c89fc1fcf29483b7b67
parent11bd1353a0b1c6f5b311a9129f2d8fc25730e241
doc: Generate, embed and animate a table of contents in the navbar itself

- extract TOC from index.html (BeautifulSoup)
- embed this into the navigation panel (again, dom manipulation)
- style it, hide it, and animate it (jquery)
doc/Makefile.common
doc/hilitesyntax.js
doc/manual.css
doc/markupSanitizer.py
doc/navmenuGenerator.py [new file with mode: 0755]