electric terminator mode broken

[megacz]

Electric terminator mode isn't working anymore with PG 4.0. When I type a period nothing happens.

[megacz]

Hrm, actually, it only happens sometimes. Something is really wrong here....

Also, previously, if the character immediately before the cursor was a period, typing a period would not add an additional period to the file. With PG 4.0 it seems to add a second period (and write-protect it!), which is unfortunate.

[megacz]

To reproduce the bug: download attached file. Type:

emacs pg-bug1.v

Twiddle your fingers while the splash screen sits there.

Type "C-c ." to turn on electric terminator.

Move the cursor to the end of the line (just AFTER) the existing period).

Type a period (".")

You will wind up with two periods in a row.

PG3.7 didn't do this.

[megacz]

/Users/megacz/pip/garrows/src/pg-bug1.v

[David Aspinall]

I can't seem to reproduce this quite as you describe.

Typing a period AFTER the existing period indeed gives the message "Can't find a parseable command" because it inserts the period, then tries to find a command which ends with .., which is incorrect, so no parseable command.

Typing a period OVER (i.e. before) the existing period processes correctly without adding a new period. I can't get PG to insert a double period unless I enable the relaxed locking mode which allows me to freely edit locked regions. If that's the case, typing a period in the locked region immediately inserts it.

Looking at the old code it's not obvious that it allowed the AFTER case either, at least not intentionally. I'll try it out and see if it's different and see whether the current behaviour could be improved, I see how it is more convenient to just go to the end of the line and hit . there.

The code here has been refactored and changed to generalise from a terminal character to a terminal string. We also had to be careful with the parsing behaviour to allow for Coq notations which use period in them (there's a ticket related to that somewhere).

[megacz]

Your second paragraph ("typing a period AFTER") is the behavior I am seeing. Proof General 3.7 did not act this way; it would refrain from inserting the second period. That was a highly desirable behavior which is now gone in Proof General 4.0. I really and truly miss that feature.

I'm confused by your second paragraph ("typing a period OVER") because in emacs when you type a character it inserts the character rather than replacing the character after the point (cursor). So you should still get a double-period there too.

Anyways, I would like the old PG3.7 behavior back, please. Thanks.

[David Aspinall]

Unfortunately have to leave this for this release, no time left now.

By OVER I was referring to appearance of block cursor in tty. Line cursor in this case is before the full-stop, i.e., char-after point is full stop. This case is the intended behaviour: not to insert a second period when one already there.

[David Aspinall]

I reconsidered. The behaviour should now be pretty close to PG 3.7, which avoids inserting semi-colons in BOTH cases. In fact so long as you're somewhere near one. It did this with a cunning but obscure implementation, the new one is more explicit but long winded.