diff options
| -rw-r--r-- | generic/pg-pbrpm.el | 2 | ||||
| -rw-r--r-- | generic/proof-script.el | 15 |
2 files changed, 11 insertions, 6 deletions
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el index 84ca0a68..6436871f 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -340,7 +340,7 @@ The prover command is processed via pg-pbrpm-run-command." (delete-frame))) ;; da: why not just this? (pop-to-buffer proof-script-buffer) - (let ((proof-one-command-per-line t)) + (let ((proof-next-command-on-new-line t)) (proof-insert-pbp-command command)))) ;; (let (span) ;; (pop-to-buffer proof-script-buffer) diff --git a/generic/proof-script.el b/generic/proof-script.el index 7bd316f4..88bfb720 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1852,14 +1852,19 @@ The optional QUEUEFLAGS are added to each queue item." ;; Moving point in proof script buffer ;; +(defun proof-next-command-new-line () + "Return non-nil if next command should start a new line." + (or proof-next-command-on-new-line ; pg-vars + (with-no-warnings (proof-ass one-command-per-line)))) + (defun proof-script-next-command-advance () "Move point to the beginning of the next command if it's nearby. Assumes that point is at the end of a command." (interactive) - (skip-chars-forward " \t\n")) -; (if (and proof-one-command-per-line (eolp)) -; (forward-line))) - + (skip-chars-forward " \t") + (if (and (eolp) + (proof-next-command-new-line)) + (forward-line))) @@ -1959,7 +1964,7 @@ No effect if prover is busy." (proof-activate-scripting) (let (span) (proof-goto-end-of-locked) - (if proof-one-command-per-line (insert "\n")) + (if (proof-next-command-new-line) (insert "\n")) (insert cmd) (setq span (span-make (proof-unprocessed-begin) (point))) (span-set-property span 'type 'pbp) |