diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-shell.el | 11 | ||||
| -rw-r--r-- | generic/proof-utils.el | 10 |
2 files changed, 15 insertions, 6 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) diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 39f139f6..eea38ce0 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -317,8 +317,7 @@ Fontifies according to the buffer's font lock defaults. Uses proof-x-symbol-decode to decode tokens if x-symbol is present. If proof-shell-leave-annotations-in-output is set, remove characters -with top bit set after fontifying so they can be used for -fontification. +with top bit set after fontifying so they don't spoil cut and paste. Returns new END value." ;; We fontify first because decoding changes char positions. @@ -392,7 +391,8 @@ Returns new END value." ;; FIXME: this function should be combined with ;; proof-shell-maybe-erase-response-buffer. (defun proof-response-buffer-display (str &optional face) - "Display STR with FACE in response buffer and return fontified STR." + "Display STR with FACE in response buffer." + ;; 3.4: no longer return fontified STR, it wasn't used. (if (string-equal str "\n") str ; quick exit, no display. (let (start end) @@ -414,7 +414,9 @@ Returns new END value." (font-lock-append-text-property start end 'face face)) ;; This returns the decorated string, but it doesn't appear ;; decorated in the minibuffer, unfortunately. - (buffer-substring start (point-max)))))) + ;; 3.4: remove this for efficiency. + ;; (buffer-substring start (point-max)) + )))) (defun proof-display-and-keep-buffer (buffer &optional pos) "Display BUFFER and mark window according to `proof-dont-switch-windows'. |