@b4n Done. I changed it a bit so the synonyms are removed even if the popup is shown because there's e.g. another symbol of the same name somewhere else.

—
Reply to this email directly or view it on GitHub.