Do we support narrowing?

[proofgeneral]

Do we support narrowing?

[hendriktews]

Hi,

my elisp manual says:

-- Function: point-min
This function returns the minimum accessible value of point in the
current buffer. This is normally 1, but if narrowing is in
effect, it is the position of the start of the region that you
narrowed to. (*Note Narrowing::.)

-- Function: point-max
This function returns the maximum accessible value of point in the
current buffer. This is `(1+ (buffer-size))', unless narrowing is
in effect, in which case it is the position of the end of the
region that you narrowed to. (*Note Narrowing::.)

Hendrik

[cpitclaudel]

Hi Hendrik,

Thanks, looks like we have the same Elisp manual :) But I'm not sure what you meant by quoting it...
Maybe I didn't make the problem clear; sorry about this. The issue is precisely the quote that you posted: PG seems to use (point-min) in many places where it should be using 1; unfortunately, (point-min) is not always 1.

Here's a screenshot that shows what happens when you step through code in a narrowed buffer:

It's easy to reproduce this: paste the following in a Coq buffer:

Lemma A: True.
Proof.
  idtac.
  idtac.
  idtac.
  idtac.
  idtac.
  idtac.
  idtac.
  idtac.

Then select a bunch of these idtacs, run narrow-to-region, run proof-goto-point, and finally undo the narrowing with widen.

Did I miss something?