improve editor dropdown

[dearing]

The editor dropdown above the current document should include more commonly used tasks, such as changing the theme and language highlighting.

[dearing]

Sadly, using select menus for themes and language highlighting does not fit well in this toolbar.

+1 dropping bootstrap