Not sure if the hotpot module is converting ampersands correctly. $heading and $title are set up differently than in other modules: instead of outputting $course->title, a temporary $title variable is created and assigned that value. That made it difficult for me to decide whether it was already formatted elsewhere or not.
Also I didn't format_string() any of the variables included in $navigation rings, because I assume these strings get processed by print_navigation(), which includes format_string().
=======================================
WARNING: DEV IS CURRENTLY VERY UNSTABLE.
This is a mega-checkin of the new Roles system. A lot of changes have
been made in core and modules.
Currently there are a lot of rough edges and known problems. We are
working hard on these .. .the reason for getting this into HEAD at this
stage is enable us to move faster (our branch was diverging from HEAD
too much).
Please keep an eye on http://docs.moodle.org/en/Roles for current status
and information for developers on how to use the new Roles system.
nicolasconnault