save-excursion again

[Uday S Reddy <u.s.reddy@cs.bham.ac.uk>]

I am just catching up belatedly with this issue of save-excursion getting 
defeated by set-buffer.  Here is my understanding.  Please let me know if I am 
missing anything.  If I have a piece of code like this that runs in a buffer A:

      (save-excursion
         (set-buffer B)
         ....X....
      )

then:

- if the code X has no possibility of getting back to the buffer A and moving 
point, then save-excursion can be replaced by save-current-buffer (and the byte 
compiler gives you a brownie point).

- if the code X has a possibility of getting back to the buffer A and moving 
around, then save-excursion should stay (despite getting smacked by the byte 
compiler).

So, every time we want to please the byte compiler, we need to prove a little 
theorem to the effect that the code X doesn't enter the buffer A?  (No doubt 
some of these theorems will be obvious.)

Cheers,
Uday