utils: improve extract_mentioned_users usefulness

Previously, extract_mentioned_users performed a regex search, converted
to a set to remove duplicates, converted that set back into a list, and
sorted the list on username, ignoring case. Every single caller of the
function then promptly took the carefully pruned and sorted result and
put it back into a set, rendering the entire exercise pointless.

In addition, every caller also resolved the usernames to database User
objects.

In this changeset, extract_mentioned_users is changed to return a set
of database User objects directly. A new extract_mentioned_usernames
function, which does only username extraction, is kept for the sole
purpose of providing a more testable interface (no database needed).

Bonus feature: The new extract_mentioned_users will prune non-existent
users, as well as the DEFAULT user. This means it is no longer possible
to @mention (and send notifications to) the DEFAULT user.