Extensions: public include

This patch defines a new type of interactions between the GUI and
so-called 'extensions'.
These extensions are dynamic plugins, that can be scripted, and they can
create GUI dialogs with widgets (like text fields, buttons, ...).