Hello Adam

Many thanks for the feedback and suggestions.  Would you be so kind as to lodge 
tickets on our trac for these?


Both issues sound like faults, in fact.  Please explain exactly which version 
of PG you are using.


 - David

On 29 Jul 2010, at 04:04, Adam Megacz wrote:

> 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

ProofGeneral mailing list

The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

Reply via email to