Semantic highlighting extensions to the IDE protocol

[ohad]

Collect proposals for extensions to the IDE protocol concerning semantic highlighting. This is currently a stub issue, hopefully we will expand it with time.

Unsafe features

Currently, the emacs mode highlights unsafe functions (believe_me, assert_total etc.), but this is not part of the protocol.
We could extend the protocol with additional messages highlighting unsafe functions, so that IDEs don't have to track them themselves.

Totality highlighting

Currently we only highlight functions, but perhaps we could differentiate whether the function is total, covering, partial.
Also for datatypes (strict positivity).

Extension

also use this information as part of error messages, e.g., if a totality check fails, we can highlight the non-decreasing cycle/call and its arguments in the partial decoration.