bug#9663: 23.2; feature wish: put priority on vcursor overlay

[Stefan Monnier <monnier@iro.umontreal.ca>]

> I still don't understand why you suggest this is a bug in Proof
> General?

I don't know either, but I do agree that uses of overlay priorities are
generally wrong (i.e. they workaround a problem, introducing others).

> I agree, most-positive-fixnum would be a reasonable choice.
> However, some day there might be a package with an overly that
> should hide the vcursor.  A large but not maximal number might be
> a better choice.

And that's the reason why I hate overlay priorities and they're never
a good solution, although once you go down that path, there's little
else you can do.

I see no need for a defcustom.  Just put a large enough value (e.g. 200)
to fix the immediate problem, and hope for the best, since after all,
that's the best we can do at this point anyway.


        Stefan