Do we support narrowing?

[cpitclaudel]

I'm seeing a lot of references to (point-min) and (point-max) in the code. @DavidAspinall, do you know if these really meant (point-min) and (point-max), or rather beginning and end of the buffer?

At the moment PG seems to break in a number of subtle ways when narrowing is in effect.

[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?