diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 1999-10-14 17:31:40 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 1999-10-14 17:31:40 +0000 |
| commit | c9225ef6b7c6623bf145a92e4481f319ee1b5259 (patch) | |
| tree | 3a82b9c7f481538ab6f6f7a25cc2e7a84373dda1 | |
| parent | 48fb5cad2583ee96b91be1a99252ebe73c1eb6e3 (diff) | |
Docstring
| -rw-r--r-- | generic/proof-shell.el | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 2b088990..cb5b5e72 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -143,7 +143,8 @@ For LEGO 1.3.1 use `nil', for Coq 6.2, use `t'.") ;; -da. (defun proof-shell-ready-prover () - "Make sure the proof assistant is ready for a command" + "Make sure the proof assistant is ready for a command. +No change to current buffer or point." (proof-shell-start) (if proof-shell-busy (error "Proof Process Busy!"))) @@ -276,11 +277,11 @@ Does nothing if proof assistant is already running." ;; up our conventions that annotations lie between 128 and ;; 256. We only observed the problem with FSF GNU Emacs 20.3 at ;; present. - (and (fboundp 'toggle-enable-multibyte-characters) - (toggle-enable-multibyte-characters -1)) + (and (fboundp 'toggle-enable-multibyte-characters) + (toggle-enable-multibyte-characters -1)) - (funcall proof-mode-for-shell) + (funcall proof-mode-for-shell) ;; Check to see that the process is still going. ;; Otherwise the sentinel will have killed off the ;; other buffers and there's no point initialising |