Stream: Proof General users

Topic: How to stop C-c C-n from going to a new line

Rudy Peterson (Jan 05 2024 at 19:43):

Every time I run proof-assert-next-command-interactive it goes to a new line.

How can I alter it so that it only goes to the end of the next command?

I added the following to my .emacs file but they don't seem to do anything:

(setq proof-next-command-insert-space nil)
(setq proof-electric-terminator-enable nil)
(setq PA-one-command-per-line nil)

Thanks!

Rudy Peterson (Jan 07 2024 at 00:01):

I figured it out I had to set:

(proof-next-command-insert-space nil)

Pierre Courtieu (Jan 07 2024 at 15:28):

Well spotted!

Last updated: Oct 13 2024 at 01:02 UTC