Hello Adam Many thanks for the feedback and suggestions. Would you be so kind as to lodge tickets on our trac for these?
http://proofgeneral.inf.ed.ac.uk/trac Both issues sound like faults, in fact. Please explain exactly which version of PG you are using. Thanks - 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 ProofGeneral@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral -- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336.
