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

From: Eli Zaretskii <[email-masked]>
Date: Wed, 11 Apr 2012 17:14:05 +0300

> From: Hendrik Tews <[email-masked]>
> Date: Wed, 11 Apr 2012 15:25:46 +0200
> Cc: Stefan Monnier <[email-masked]>,
>     [email-masked],
>     [email-masked],
>     [email-masked]
> 
>    > 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.