<source> is deprecated, but not removed yet. I think it should not be removed from the documentation as long as it works—feel free to add a huge warning advising users not to use it, but not mentioning it while it’s still used on all over Wikimedia creates even larger confusion than what was before. For example a user may wonder why a page ends up in Category:Pages with syntax highlighting errors when there’s no
<syntaxhighlight> on the page at all (only
<source> tags); if
<source> is also mentioned, it’s more clear the two are synonyms (at this time).