update seti theme. fixes #118912

This commit is contained in:
Martin Aeschlimann 2021-03-15 22:13:06 +01:00
parent 7f43e5c846
commit 51a15dee0a
3 changed files with 302 additions and 277 deletions

View file

@ -182,6 +182,16 @@ function darkenColor(color) {
return res;
}
function mergeMapping(to, from, property) {
if (from[property]) {
if (to[property]) {
to[property].push(...from[property]);
} else {
to[property] = from[property];
}
}
}
function getLanguageMappings() {
let langMappings = {};
let allExtensions = fs.readdirSync('..');
@ -204,7 +214,22 @@ function getLanguageMappings() {
if (Array.isArray(filenames)) {
mapping.fileNames = filenames.map(function (f) { return f.toLowerCase(); });
}
langMappings[languageId] = mapping;
let existing = langMappings[languageId];
if (existing) {
// multiple contributions to the same language
// give preference to the contribution wth the configuration
if (languages[k].configuration) {
mergeMapping(mapping, existing, 'extensions');
mergeMapping(mapping, existing, 'fileNames');
langMappings[languageId] = mapping;
} else {
mergeMapping(existing, mapping, 'extensions');
mergeMapping(existing, mapping, 'fileNames');
}
} else {
langMappings[languageId] = mapping;
}
}
}
}
@ -216,6 +241,8 @@ function getLanguageMappings() {
return langMappings;
}
exports.copyFont = function () {
return downloadBinary(font, './icons/seti.woff');
};

File diff suppressed because it is too large Load diff