diff options
| author | David Aspinall | 1998-11-12 14:37:23 +0000 |
|---|---|---|
| committer | David Aspinall | 1998-11-12 14:37:23 +0000 |
| commit | fda517f5cf111ec1caf132c6580b2859baf61bc5 (patch) | |
| tree | 09e8159dd4a13e715b860281c71e7075e8a6ed6d | |
| parent | 75441a61e232861c4536b94ca462d3783d6c27e8 (diff) | |
Rashly fixed a suspicious looking nested use of set-buffer. Docstrings.
| -rw-r--r-- | generic/proof-shell.el | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index a42de00d..c6a767e5 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -541,7 +541,8 @@ we call `proof-shell-handle-error-hook'. " (defun proof-shell-handle-interrupt () (save-excursion - (display-buffer (set-buffer proof-pbp-buffer)) + (set-buffer proof-pbp-buffer) + (display-buffer proof-pbp-buffer) (goto-char (point-max)) (newline 2) (insert-string @@ -930,10 +931,10 @@ how far we've got." ;; da: What is the rationale here for making the *command* sent ;; invisible, rather than the stuff returned???? -;; doc string makes no sense of this. +;; old doc string said "without responding to the user" which was wrong. ;; FIXME: note: removed optional 'relaxed' arg (defun proof-shell-invisible-command (cmd) - "Send cmd to the proof process without responding to the user." + "Send CMD to the proof process without revealing it to the user." (proof-shell-ready-prover) (if (not (string-match proof-re-end-of-cmd cmd)) (setq cmd (concat cmd proof-terminal-string))) |