Change the server-side push rule to check for formatted_body in addition to body

[composite9239]

This proposal is based on this issue: element-hq/element-web#28335

If it is true that the server-side push rule only checks for body, then users who disable display name notifications but enable username notifications still do not get notified for pill mentions. Rather, they are only notified for the localpart of their Matrix ID.

It seems dubious whether any user would actually desire to be notified for specifically the localpart of their Matrix ID outside of the context of their full Matrix ID, whether that full Matrix ID be manually written out in body as @user:example.com or in formatted_body as an included a href=\"https://matrix.to/#/@user:example.com\". Regardless, the latter scenario seems critical to make functional for username notifications because pill mentions are so common in Element.

It is also not all that unusual that someone would want to only be notified for username mentions and not display name mentions. For example, if someone's display name is "Happy," they do not necessarily want to be notified every time someone says "I am happy." They do want to be notified when people mention them in pill form, but right now this does not appear to be possible if display name notifications are disabled. They have to choose between receiving notifications for all instances of "happy" or none at all, including their being tagged in pill form.

I welcome any correction, and my apologies for any misunderstanding.

[clokep]

Mentions parsing the body are legacy mentions, see https://spec.matrix.org/v1.12/client-server-api/#user-and-room-mentions which defines the m.mentions property.

MSC4210 aims to remove the old way.

I don't think there's anything to do here.