Custom Query (361 matches)

The Coq/ProofGeneral/Emacs? interactive functions coq-insert-command, coq-insert-tactic, coq-insert-tactical and coq-insert-term fail if the text read is empty.

For example if we type [C-c C-a C-t RET] (at the end of a Coq buffer), Emacs raises the following low-level error:

let: Wrong type argument: integer-or-marker-p, nil

which is somewhat distracting.

On the one hand, we could add a test in coq-insert-from-db that raises a custom error instead, like the one raised by [M-x RET]... For instance, we could raise something like:

(error "No %s name given" (downcase prompt))

whenever (string= tac "").

But on the other hand, one could prefer not to raise any extra error, all the more so as there is actually a bug in coq-command-at-point (ultimately called by the indentation asked by coq-insert-from-db).

Indeed, the former error is also raised if we just type TAB at the end of a Coq buffer, because the last line of coq-command-at-point fails when st is nil. We should replace that line with:

(if st (buffer-substring st (+ nd 1)) "") )))

or just with:

(and st (buffer-substring st (+ nd 1))) )))

Kind regards, Erik Martin-Dorel.

Hi,

the attached patch fixes the documentation of the special Isabelle (2007) key bindings in doc/ProofGeneral.texi with respect to isar/isar.el.

The Proof General version against which the patch was made was

ProofGeneral-3.7pre080117.

Hello, I am getting an error with bytecode of the 4.0 package and emacs-23.1.1.

I perform the following:

download pg at http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-4.0.tgz

untar, set path variable of emacs correctly. Start emacs, open a .v file. Here is the error message:

Loading coq... Coq default abbrevs loaded Loading coq...done File mode specification error: (wrong-number-of-arguments called-interactively-p 1)

Notice that if I make clean; make in pg directory everything goes well.

Regards, PC