diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2001-12-10 19:12:26 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2001-12-10 19:12:26 +0000 |
| commit | 33d4e28e7ab736a73313fb00db3dcb65d1b8fbe7 (patch) | |
| tree | 6f6e649571d81a4fd53dc3375c9500310abf8346 /generic/proof-shell.el | |
| parent | 5721c119ad270b128f8770afbef8a691befd4ed0 (diff) | |
Dont return a fontified string in proof-response-buffer-display.
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 11 |
1 files changed, 9 insertions, 2 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 60bcd2d7..4f2b1678 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -227,6 +227,9 @@ Does nothing if proof assistant is already running." (save-excursion (set-buffer proof-shell-buffer) + ;; PG 3.4: clear output from previous sessions. + (erase-buffer) + ;; FIXME: Disable 16 Bit ;; We noticed that for LEGO, it otherwise converts annotations ;; to characters with (non-ASCII) code around 3000 which screws @@ -255,6 +258,9 @@ Does nothing if proof assistant is already running." (and (fboundp 'toggle-enable-multibyte-characters) (toggle-enable-multibyte-characters -1)) (funcall proof-mode-for-goals)) + ;; + ;; If the process died, switch to the buffer to + ;; display the error messages to the user. (switch-to-buffer proof-shell-buffer) (error "%s process exited!" proc))) (message "Starting %s process... done." proc)))) @@ -763,8 +769,9 @@ last match in the buffer for END-REGEXP. The match for END-REGEXP is not part of the specified region. This mechanism means if there are multiple matches for START-REGEXP and END-REGEXP, we match the largest region containing them all. -This is a subroutine of proof-shell-handle-error. -Returns the string (with faces) in the specified region." +This is a subroutine of proof-shell-handle-error." +;; 3.4: doesn't return the string any more. +;; Returns the string (with faces) in the specified region." (let (start end string) (save-excursion (set-buffer proof-shell-buffer) |