d686674eca
Since both the file tags and workspace tags are sorted, it is unnecessary to completely resort the tags for the workspace - instead, remove the tags belonging to the file from the workspace tags and merge the updated file's tags into the workspace tags. The merge is optimized for merging small number of tags into a large array. For instance, the total number of tags in linux kernel is about 2300000 while the average number of tags per file is about 65 (35000 source files). Most of the time merge won't be performed so we can avoid expensive string comparisons and try to make bigger jumps to see if some merge is needed or not (more details in the source file comments).