menu.html.php. This serves two purposes:
1) It's more efficient since we're doing less passes over the Menu tree
2) We're allowing themers to decide whether or not to show empty menus
can override them and define their own menu formats. I worry a little
bit that this approach may be too heavy since we're now doing a lot
more template includes than we were before. Also, I had to change the
Menu API to stop using __toString() because you can't throw exceptions
from __toString() which would make it an unhappy experience for
developers.
