Distracting error (actually raised by coq-command-at-point)

[Erik Martin-Dorel]

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.

[David Aspinall]

coq-command-at-point patched as suggested. Many thanks!