diff options
Diffstat (limited to 'ext/bg/js/util.js')
| -rw-r--r-- | ext/bg/js/util.js | 17 | 
1 files changed, 17 insertions, 0 deletions
| diff --git a/ext/bg/js/util.js b/ext/bg/js/util.js index a0fca270..a37e223c 100644 --- a/ext/bg/js/util.js +++ b/ext/bg/js/util.js @@ -96,6 +96,23 @@ function sortTermDefs(definitions) {      });  } +function undupeTermDefs(definitions) { +    const definitionGroups = {}; +    for (const definition of definitions) { +        const definitionExisting = definitionGroups[definition.id]; +        if (!definitionGroups.hasOwnProperty(definition.id) || definition.expression.length > definitionExisting.expression.length) { +            definitionGroups[definition.id] = definition; +        } +    } + +    const definitionsUnique = []; +    for (const key in definitionGroups) { +        definitionsUnique.push(definitionGroups[key]); +    } + +    return definitionsUnique; +} +  function buildTag(name, meta) {      const tag = {name};      const symbol = name.split(':')[0]; |