Hoist DevTools launcher into a JS function (#334)

Closes #330

Users can now launch DevTools by running `$launchDevTools` in the console. They can easily add a bookmark to do this evaluation.

Author: grouma