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

[Hendrik Tews]

Eli Zaretskii writes:
   Date: Wed, 11 Apr 2012 15:22:47 +0300
   Subject: Re: bug#9663: 23.2; feature wish: put priority on vcursor overlay
   
   > From: Hendrik Tews <tews@os.inf.tu-dresden.de>
   > Date: Wed, 11 Apr 2012 13:54:40 +0200
   > Cc: Kevin Rodgers <kevin.d.rodgers@gmail.com>, 9663@debbugs.gnu.org
   > 
   > Lars Magne Ingebrigtsen writes:
   >    Date: Wed, 11 Apr 2012 13:35:18 +0200
   >    Subject: Re: bug#9663: 23.2; feature wish: put priority on vcursor 
overlay
   >    
   >    Hendrik Tews <tews@os.inf.tu-dresden.de> writes:
   >    
   >    >    same priority. Which makes me wonder: why other overlay have
   >    >    you bumped into which has either higher priority than nil, or
   >    >    nil priority but is not larger than vcursor.
   >    >
   >    > As I wrote in the feature wish: the locked region in Proof
   >    > General (proof-locked-span). It has priority 100, see the call to
   >    > span-raise inside proof-init-segmentation in
   >    > generic/proof-script.el.
   >    
   >    So perhaps this is a bug in Proof General and doesn't really require an
   >    overlay priority in Emacs?
   > 
   > 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?

   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. A large but not maximal number might be
a better choice.

   And if we agree this is TRT, do we still need a defcustom?

Because the defcustom gives more freedom to users and without it
they have to resort to 

   (defadvice vcursor-move (after vcursor-overlay-set-priority activate)
     "Change the priority of the vcursor overlay."
     (and vcursor-overlay
          (overlay-put vcursor-overlay 'priority 1000)))

Bye,

Hendrik