bug#4911: mouse-face property should merge face attributes, not replace

[Drew Adams]

> > mouse-face property seems ugly: it simply overwrites the face property
> > for characters under the mouse.  For example in Info, blue underlined
> > links turn black without the underline when the mouse is hovered over
> > them to give the green background from the highlight face.  This feels
> > unnatural.
> >
> > mouse-face property on programming language text which is heavily
> > decorated with font-lock.  Users complain that when the mouse is over
> > a region the normal fontification is obliterated.

FWIW, I don't think it's ugly, and I don't think the
underlying (non mouse-face) face attributes show show
(be merged).

IOW.  I'm one user who prefers the current (longstanding)
behavior.  Just one opinion.

> I think it might make sense to merge the properties...  but, on the
> other hand, this may make the text illegible.

Not just less legible.  Different (conflicting) purposes.

It's easy enough to move the mouse, to see the non-hover
face.  Why would one suppose that someone wants to merge
that face with `mouse-face'?

Remember too that `mouse-face' can have any face properties
- you are talking about merging arbitrary faces.

Just what is the motivation, besides someone feeling the
behavior is "ugly"?

That font-lock highlighting doesn't show when there's a
link (or some other use of `mouse-face') is a feature,
not a bug.  Why do Proof General users need to see both
kinds of highlighting at the same time?  And merging
could, at least in some cases, make noticing the link etc.
difficult.

To me, it sounds like Proof General should look for
another solution to the problem presented.