First of all, big thanks to the Proof General team for creating such a 
wonderful piece of software!  I really can't imagine interactive theorem 
proving without it, and I appreciate the effort all the more considering that 
the kind of people who use theorem provers would probably rather be spending 
their time programming in languages other than emacs lisp!

I'm a big fan of the "electric terminator" feature.  Is there any way to get 
the "electric terminator" behavior to apply only when the cursor is in a region 
which is not a comment?  Emacs knows which regions these are (from the syntax 
coloring), and it would make it much easier to type prose text with periods in 
it within the comments of a Coq file.  I checked the manual but couldn't find a 
setting for this.


  - a

PS, is there any way to get Proof General *not* to attempt to process a file 
immediately upon it being opened?  IIRC old versions of Proof General were like 
this.  I wasn't quite sure what this setting would be called, so it was a bit 
difficult to find it in the manual (I'm sure it's in there).  A lot of the 
scripts I've been working on lately cause Coq to go into an infinite loop, and 
the region of text with the offending command in it becomes locked (read-only) 
immediately, so I have to use an editor other than emacs (or disable 
ProofGeneral, or rename the file to another extension) in order to fix a file 
once I've accidentally typed such a 
ProofGeneral mailing list

Reply via email to