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

[Eli Zaretskii]

> From: Hendrik Tews <tews@os.inf.tu-dresden.de>
> Date: Wed, 11 Apr 2012 15:25:46 +0200
> Cc: Stefan Monnier <monnier@iro.umontreal.ca>,
>     larsi@gnus.org,
>     kevin.d.rodgers@gmail.com,
>     9663@debbugs.gnu.org
> 
>    > Could you explain why using a non-deprecated feature (priorities
>    > of overlays) is a bug?
>    
>    It isn't.  
> 
> I still don't understand why you suggest this is a bug in Proof
> General?

But I just said it was NOT a bug, not in Proof General, not anywhere.

>    However, if, as you say, vcursor should always be visible,
>    why not make its default priority most-positive-fixnum?  
> 
> 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.

We can bother about that when that day comes, if it ever does.

> A large but not maximal number might be a better choice.

Any other value is arbitrary, and I don't like arbitrary values.

But since it sounds like I'm the only one, I will have to live with
that.