Make pickers functional

The $generate.pickers parameter can currently be used to generate language & file format pickers for generated HTML documents. However, the parameter is off by default and the current pickers are only dummies.

What needs to be solved:

• Find a solution for adding correct (non-dummy) values to the pickers
  • Language: language codes or language name | URL
  • Format: format code (html|singlehtml|pdf|epub) | URL
• Packages can usually either be installed locally or copied to a web server, this means:
  • either the same mechanism needs to cover both cases or that the information needs to be easily editable
  • a centralised server-based approach might not be the best option (since that would not play nice with locally installed documentation)

Options:

• pure HTML written directly into the documents when building
• JSON (or XML) file written when building but editable at any time
• central JSON (or XML) file on a server that covers all products (= quite large) and is referenced from all files (thus, editable at any time and without having to update the HTML files themselves)