#74 closed defect (wontfix)
Coq: bug in electric terminator: typing '.' in comment causes comment to be sent and locked
| Reported by: | David Aspinall | Owned by: | David Aspinall |
|---|---|---|---|
| Priority: | major | Milestone: | PG-Emacs-3.7 |
| Component: | 2:pg-emacs | Keywords: | |
| Cc: |
Description
When I type a '.' within a comment, the comment is sent to Coq and then locked. This is obviously not what I want! A '.' within a comment should be ignored.
Emacs : GNU Emacs 22.0.93.1 (x86_64-redhat-linux-gnu, GTK+ Version 2.10.9)
of 2007-02-13 on hs20-bc1-6.build.redhat.com
Package: Proof General
current state: ============== (setq
proof-general-version "Proof General Version 3.6pre061107. Released by da." proof-assistant "Coq" )
Note: See
TracTickets for help on using
tickets.
I can't reproduce this as described, i.e. typing a terminator inside a comment does not attempt to lock that comment. E.g., for the trivial file
test.vtyping this with electric terminator turns on scripting mode but does not attempt to lock the unclosed comment. However, typing in this file:
results in the first comment being locked (and cursor moved, unfortunately) when the second one is typed. This is mildly annoying and should be fixed, but as the idea of electric terminator is to lock-as-you-type - so previous text should already be processed - it doesn't seem too bad.
Closing as wontfix for now. Patches to improve behaviour welcome.