Custom Query (361 matches)

Indentation is not closed properly after an "Abort." statement, following "Theorem".

Simple fix: In coq/coq-syntax.el: Add "Abort" to the list of keywords defined in coq-keywords-save-strict (line 618 in ProofGeneral-3.7pre071025).

While editing a Coq script proof file, the indentation does not work. In proof-General->Advanced-> Customize ->Proof user options, the Coq script ident option is activated. When I press tab, or M-x indent-according-to-mode, or M-x ident-region, I receive the message "Symbol's value as a variable is void: script-indent"

Indentation works well in other mode like Tuareg

I'm runing emacs 22.1.1 (i486-pc-linux-gnu, GTK+ Version 2.12.0) with ProofGeneral-3.7pre080117 and The Coq Proof Assistant, version 8.1pl3 (Dec. 2007)

PG-Emacs: 3.7pre071112 Isabelle: 2007

Here is a reproducible way to get ProofGeneral 3.7pre071112 out of sync with the isabelle2007 process, simply process this theory:

theory Scratch imports Main begin

lemma X: "a=b ==> b=a" by simp -- "Text with \illegal escape sequence"

end

This happens quite often if you insert latex in your formal comment and forget to convert "..." to {*...*} syntax. Having to restart Isabelle each time is annoying for large theories.