Here is an updated patch for the “grep headings” feature.

As discussed before, I introduced a text property so that one can tell
without guessing which parts of the compilation buffer are not coming
from the external process.  This seems to supersede the
'compilation-header-end' property introduced by Lars in commit
07f748da43, so I replaced its uses by the new 'compilation-aside'
property.  I could easily revert that, but it seemed reasonable to
uniformize things in this case.

I've also incorporated all other suggestions from other messages.  (And
Juri, nevermind what I said about some faces, it only applies to the
Modus theme.)