Menu "options" block is now deprecated. Move members to "config"!

* Deprecate & allow conversion behind the scenes for now + add warning in log
* Add some initial docs
* Clean up prompt.hjson and menu.hjson

core/theme.js

@@ -571,7 +571,7 @@ function displayThemedPrompt(name, client, options, cb) {
                 //  doing so messes things up -- most terminals that support font
                 //  changing can only display a single font at at time.
                 //
-                const dispOptions = Object.assign( {}, options, promptConfig.options );
+                const dispOptions = Object.assign( {}, options, promptConfig.config );
                 //  :TODO: We can use term detection to do nifty things like avoid this kind of kludge:
                 if(!options.clearScreen) {
                     dispOptions.font = 'not_really_a_font!';    //  kludge :)