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. Thanks, - 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 command._______________________________________________ ProofGeneral mailing list ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral
