chore: Rename some ExtensionsGallery to ExtensionMarketplace

Issue: Standardize extensions marketplace terminology (gitlab#512642 - closed)

• Part 1: chore: Rename some ExtensionsGallery to Extensi... (!424 - merged)
• Part 2: chore: Rename `WebIdeConfig.extensionsGallerySe... (!425 - merged)
• Part 3: chore: Finish renaming "gallery" to "marketplace" (!426 - merged)

What does this MR do and why?

chore: Rename some ExtensionsGallery to ExtensionMarketplace

• This supports this effort
• The rest of renaming will happen in later commits