Issue #3633989: Add navigation/top bar toggle tool

Adds a Hide navigation tool to the top bar: a button with a tilde icon that hides the navigation sidebar and the top bar, and shows them again; the backtick key does the same. While they are hidden the button floats in the top left corner, with options to hide its label and to hide the button itself. The state is kept per browser tab in session storage. See the README section Hide navigation.

Closes #3633989