How can I get C-c C-n to format the current line in proof-general coq-mode-map

Question

I'm using proof-general to write Coq proofs.

When I use C-c C-n in a proof, my cursor is moved to the next line, but the current line is not formatted. So for instance, if I type:

intros n. <C-c C-n>

my cursor moves to the next line, but intros n. remains unindented. So I have to go back up a line, go to the end of the line and hit <RET> to auto-indent the coq statement. At which point, proof-general considers that statement changed and I have to re-run it.

Ideally, I would line C-c C-n to auto-indent the line it is running and to not go to the next line.

How can I make that happen?

Answer 1

You can do what you're describing using advice:

(advice-add 'proof-assert-next-command-interactive :before
            (lambda (&rest args) (indent-for-tab-command)))

… but I suspect this is an AB problem: C-c C-n doesn't insert a newline, so if you're writing proofs you will in fact press RET roughly once per time you press C-c C-n. If you press it before pressing C-c C-n, then the line will be properly indented.

Worse, you shouldn't typically have an incorrectly indented intros in the first place, if you're using the default setup (electric-indent): whichever parent line is causing intros to need indentation should also cause it to be indented when its line is created.

If I misunderstood, please do update the OP with a concrete example of the scenario that leads you to needing this feature, and we can see whether there is already something in PG that might help.

Answer 2

I was also thinking about advice-add as suggested by @Clément, but actually I believe the OP's suggestion is rather a bug-fix than a feature wish…:

When we type C-c C-n just before adding a newline with RET, if the line is not already properly indented (which can occur if this line was edited not after typing RET previously on the line before, which can occur in practice), the C-c C-n action is distractedly removed… so we need to redo C-c C-n anew.

So I've just opened a tentative PR in https://github.com/ProofGeneral/PG/pull/604, @azani and @Clément: feel free to comment/review there when you have some time.