Theme menus
-----------
-Complicated themes, especially those dealing with `HTML inputs <html>`,
+Complicated themes, especially those dealing with :doc:`HTML inputs <html>`,
may have needs for user control that go beyond those of transition buttons.
(An obvious example may be “reload the HTML file”.) For this reason,
themes can also set simple *theme menus*, which are always visible