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.