Handle user renames in rendering @-mentions #1258
Description
Currently we render @-mentions using the user's name as recorded in the HTML. If the mentioned user has edited their name since the message was sent (or was last edited), this will be their old name. Instead, we should show the mentioned user's current name.
To do this we'll use the mentioned user's ID, which is also encoded in the HTML of the @-mention. Then we can look that up in our users data. If the user is unknown, we can fall back to the name that's in the HTML.
This behavior is specified in docs just written today:
https://zulip.com/api/message-formatting#mentions
(or maybe this link; added in zulip/zulip@3aa2671), but I believe it's been the web app's behavior for a long time.