[Top][All Lists]
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
bug#9663: 23.2; feature wish: put priority on vcursor overlay
|
From: |
Eli Zaretskii |
|
Subject: |
bug#9663: 23.2; feature wish: put priority on vcursor overlay |
|
Date: |
Wed, 11 Apr 2012 17:14:05 +0300 |
> From: Hendrik Tews <address@hidden>
> Date: Wed, 11 Apr 2012 15:25:46 +0200
> Cc: Stefan Monnier <address@hidden>,
> address@hidden,
> address@hidden,
> address@hidden
>
> > 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.