Custom Query (361 matches)
Results (76 - 78 of 361)
Ticket | Resolution | Summary | Owner | Reporter |
---|---|---|---|---|
#173 | fixed | coq indenting mode gets confused by *) in proofs | ||
Description |
Using the latest CVS version of pg-emacs (as of Thu Jan 24 16:48:42 PST 2008), enter the following Coq script: Theorem p : forall (P : Prop), P -> P. Proof. try (simpl in *). intros P H. apply H. Qed.
This is legal Coq code, but the occurrence of the sequence |
|||
#174 | fixed | Unable to exit prover | ||
Description |
When using ProofGeneral with XEmacs 21.4 and the CVS version of Isabelle, it is not possible to exit the prover by selecting the "Isabelle -> Exit Isabelle" menu item. Instead of terminating the prover, ProofGeneral just displays the message "Warning: buffer *isabelle* not killed; still associated with prover process.". This problem does not occur with XEmacs 21.5, though. |
|||
#175 | fixed | ProofGeneral accidentally resets itself while scrolling | ||
Description |
When using ProofGeneral with XEmacs 21.4 and the CVS version of Isabelle, the following problem occurs: when stepping through a theory file using the "Next" button, ProofGeneral sometimes accidentaly resets itself when the cursor hits the bottom of the window in which the theory file is displayed, and XEmacs tries to scroll the text in the window. The effect of this bug is that the part of the theory file that was already processed is no longer coloured blue, and ProofGeneral's internal pointer indicating the next command to be processed is reset to the beginning of the theory file, causing the Isabelle process and ProofGeneral to get completely out of sync. In addition, the error message "(1) (error/warning) Error in 'post-command-hook' (setting hook to nil): (error Lisp nesting exceeds 'max-lisp-eval-depth')" is displayed. This problem does not occur with XEmacs 21.5, though. |