diff options
| -rw-r--r-- | generic/proof-shell.el | 138 | ||||
| -rw-r--r-- | generic/proof-x-symbol.el | 112 | ||||
| -rw-r--r-- | generic/proof.el | 30 |
3 files changed, 169 insertions, 111 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index ba32e565..5f9794f7 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -597,7 +597,7 @@ If there is no command under the mouse, behaves like mouse-track-insert." (&optional erase-next-time clean-windows force) "Erase the response buffer according to proof-shell-erase-response-flag. ERASE-NEXT-TIME is the new value for the flag. -If CLEAN-WINDOWS is set, use proof-clear-buffer to do the erasing. +If CLEAN-WINDOWS is set, use proof-clean-buffer to do the erasing. If FORCE, override proof-shell-erase-response-flag. If the user option proof-tidy-response is nil, then @@ -676,20 +676,21 @@ extents." ;; We should only clear the output that was displayed from ;; the *previous* prompt. - ;; da: I get a lot of empty response buffers displayed - ;; which might be nicer removed. Temporary test for - ;; this clean-buffer to see if it behaves well. + ;; FIXME da: I get a lot of empty response buffers displayed + ;; which might be nicer removed. Temporary test for this + ;; clean-buffer to see if it behaves well. - ;; NEW!! ;; Erase the response buffer if need be, maybe also removing the - ;; window. Indicate that it should be erased before the next output. + ;; window. Indicate that it should be erased before the next + ;; output. (proof-shell-maybe-erase-response t t) (set-buffer proof-goals-buffer) - ;; NEW!! 10.12.98 Keep point at beginning of buffer instead - ;; of end. Might be nicer to keep it at "current" subgoal - ;; a la Isamode, but never mind. + + ;; Might be nicer to keep point at "current" subgoal a la + ;; Isamode, but never mind. (erase-buffer) + (newline) ; waste a line ;; Insert the (possibly cleaned up) string. (if proof-shell-leave-annotations-in-output @@ -699,18 +700,18 @@ extents." ;; Get fonts and characters right (proof-fontify-region (point-min) (point-max)) + (set-buffer-modified-p nil) ; nicety + (proof-display-and-keep-buffer proof-goals-buffer (point-min)) - ;; FIXME: - ;; This code is broken for Emacs 20.3 which has 16 bit - ;; character codes. (Despite earlier attempts to make - ;; character codes in this buffer 8 bit) - ;; But this is a more general problem in Proof General + ;; FIXME: This code is broken for Emacs 20.3 (mule?) which has + ;; 16 bit character codes. (Despite earlier attempts to make + ;; character codes in this buffer 8 bit) + ;; But this is a more serious future problem in Proof General ;; which requires re-engineering all this 128 mess. - ;; FIXME Mk II: - ;; This is also going to be broken for X-Symbol interaction, - ;; when tokens (several chars long) are replaced by single - ;; characters. + ;; FIXME Mk II: This is also going to be broken for X-Symbol + ;; interaction, when tokens (several chars long) are replaced by + ;; single characters. (unless ;; Don't do it for Emacs 20.3 or any version which ;; has this suspicious function. @@ -800,6 +801,7 @@ 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." (let (start end string) (save-excursion @@ -809,6 +811,9 @@ Returns the string (with faces) in the specified region." (goto-char (marker-position proof-marker)) (setq start (- (search-forward-regexp start-regexp) (length (match-string 0)))) + ;; FIXME: if the shell buffer is x-symbol minor mode, + ;; this string can contain X-Symbol characters, which + ;; is not suitable for processing with proof-fontify-region. (setq string (if proof-shell-leave-annotations-in-output (buffer-substring start end) @@ -838,24 +843,32 @@ See the documentation for `proof-shell-delayed-output' for further details." ;; Anyway, we leave it alone now, maybe to see some spurious ;; "done" displays + ;; FIXME: this can be done away with, probably. (unless proof-shell-leave-annotations-in-output (setq str (proof-shell-strip-special-annotations str))) - - (with-current-buffer proof-response-buffer - ;; FIXME da: have removed this, possibly it junks - ;; relevant messages. Instead set a flag to indicate - ;; that response buffer should be cleared before the - ;; next command. - ;; (erase-buffer) - - ;; NEW! - ;; Erase the response buffer if need be, and indicate that - ;; it is to be erased again before the next message. - (proof-shell-maybe-erase-response t nil) - (setq pos (point)) - (insert str) - (proof-fontify-region pos (point)) - (proof-display-and-keep-buffer proof-response-buffer))) + + (proof-shell-maybe-erase-response t nil) + (proof-response-buffer-display str) + (proof-display-and-keep-buffer proof-response-buffer)) + + ;; old code duplicated much of proof-response-buffer-display + +; (with-current-buffer proof-response-buffer +; ;; FIXME da: have removed this, possibly it junks +; ;; relevant messages. Instead set a flag to indicate +; ;; that response buffer should be cleared before the +; ;; next command. +; ;; (erase-buffer) + +; ;; NEW! +; ;; Erase the response buffer if need be, and indicate that +; ;; it is to be erased again before the next message. +; (proof-shell-maybe-erase-response t nil) +; (goto-char (point-max)) +; (setq pos (point)) +; (insert str) +; (proof-fontify-region pos (point)) +; (proof-display-and-keep-buffer proof-response-buffer))) ;; ;; 2. Text to be inserted in goals buffer ;; @@ -902,13 +915,21 @@ The error message is displayed in the `proof-response-buffer'. Then we call `proof-shell-handle-error-hook'. " ;; flush goals - (or (equal proof-shell-delayed-output (cons 'insert "Done.")) - (save-excursion ;current-buffer - (set-buffer proof-goals-buffer) - (erase-buffer) - (insert (cdr proof-shell-delayed-output)) - (proof-fontify-region (point-min) (point-max)) - (proof-display-and-keep-buffer proof-goals-buffer))) + (unless + (equal proof-shell-delayed-output (cons 'insert "Done.")) + (save-excursion + ;; da: Maybe we don't know it's a perfect string for analysis, + ;; but give it a shot anyway. + (proof-shell-analyse-structure + (cdr proof-shell-delayed-output)))) +; old code duplicated first part of analyse-structure. +; (save-excursion ;current-buffer +; (set-buffer proof-goals-buffer) +; (erase-buffer) +; (newline) +; (insert (cdr proof-shell-delayed-output)) +; (proof-fontify-region (point-min) (point-max)) +; (proof-display-and-keep-buffer proof-goals-buffer))) ;; This prevents problems if the user types in the ;; shell buffer: without it the same error is seen by @@ -1074,7 +1095,9 @@ particularly in proof-start-queue and proof-shell-exec-loop." ;; Lego uses this hook for setting the pretty printer ;; width, Coq uses it for sending an initialization string ;; (although it could presumably use proof-shell-init-cmd?). - ;; Plastic uses this hook to remove literate-style markup from 'string'. + ;; Plastic uses it to remove literate-style markup from 'string'. + ;; x-symbol mode uses this hook to convert special characters into + ;; tokens for the proof assistant. (run-hooks 'proof-shell-insert-hook) ;; Now we replace CRs from string with spaces. This was done in @@ -1098,6 +1121,8 @@ particularly in proof-start-queue and proof-shell-exec-loop." (insert string) (set-marker proof-marker (point)) + ;; FIXME da: this space fudge is actually a visible hack: + ;; the response string begins with a space and a newline. (insert proof-shell-insert-space-fudge) (comint-send-input))) @@ -1510,9 +1535,9 @@ however, are always processed; hence their name)." ;; Now we're looking for the end of the piece of output ;; which will be processed. - ;; Note that the way this filter works, - ;; only one piece of output can be dealt with at a time - ;; so we loose sync if there's more than one bit there. + ;; Note that the way this filter works, only one piece of + ;; output can be dealt with at a time so we loose sync if + ;; there's more than one bit there. ;; The blasphemous situation that the proof-action-list ;; is empty is now quietly ignored so that users can @@ -1523,27 +1548,31 @@ however, are always processed; hence their name)." ;; Note that any "unexpected" output like this gets ;; ignored. (if proof-action-list - (let ((startpos (goto-char (marker-position proof-marker))) - (urgnt (marker-position + (let ((urgnt (marker-position proof-shell-urgent-message-marker)) - string) + string startpos) ;; Ignore any urgent messages that have already been ;; dealt with. This loses in the case mentioned above. ;; A more general way of doing this would be ;; to filter out or delete the urgent messages which ;; have been processed already. + (setq startpos (goto-char (marker-position proof-marker))) (if (and urgnt - (< (point) urgnt)) - (setq startpos (goto-char urgnt))) + (< startpos urgnt)) + (setq startpos (goto-char urgnt)) + ;; Otherwise, skip possibly a (fudge) space and new line + (if (eq (char-after startpos) ?\ ) + (setq startpos (goto-char (+ 2 startpos))) + (setq startpos (goto-char (1+ startpos))))) ;; Find next prompt. (if (re-search-forward proof-shell-annotated-prompt-regexp nil t) (progn (backward-char (- (match-end 0) (match-beginning 0))) ;; FIXME: decoding x-symbols here is perhaps a bit - ;; expensive; but perhaps we could cut and paste - ;; from here to the goals buffer to - ;; avoid duplicating effort? + ;; expensive; moreover it leads to problems + ;; processing special characters as annotations + ;; later on. So no fontify or decode. ;; (proof-fontify-region startpos (point)) (setq string (buffer-substring startpos (point))) (goto-char (point-max)) @@ -1743,7 +1772,8 @@ processing." (save-excursion (set-buffer proof-shell-buffer) - (proof-font-lock-configure-defaults) + ;; We do not enable font-lock here + ;; (proof-font-lock-configure-defaults) (let ((proc (get-buffer-process proof-shell-buffer))) ;; Add the kill buffer function and process sentinel diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el index f2d612d7..bd78d22c 100644 --- a/generic/proof-x-symbol.el +++ b/generic/proof-x-symbol.el @@ -18,7 +18,8 @@ ;;; ###autoload (defun proof-x-symbol-support-maybe-available () "A test to see whether x-symbol support may be available." - (and (eq (console-type) 'x) + (and (boundp 'console-type) ; FSF Emacs doesn't have this + (eq (console-type) 'x) ; (neither does it have x-symbol) (condition-case () (require 'x-symbol-autoloads) (t (featurep 'x-symbol-autoloads))))) @@ -50,7 +51,7 @@ If ERROR is non-nil, give error on failure, otherwise a warning." (funcall error-or-warn "Proof General: x-symbol package must be installed for x-symbol-support! The package is available at http://www.fmi.uni-passau.de/~wedler/x-symbol")) - ((not (eq (console-type) 'x)) + ((not (and (boundp 'console-type) (eq (console-type) 'x))) (funcall error-or-warn "Proof General: x-symbol package only runs under X!")) ((or (not (fboundp 'x-symbol-initialize)) @@ -160,55 +161,25 @@ A value for proof-shell-insert-hook." (prog1 (buffer-substring) (kill-buffer (current-buffer))))))) -;; ### autoload -(defun proof-x-symbol-mode () - "Turn on/off x-symbol mode in current buffer, from proof-x-symbol-enable." - (interactive) - (save-excursion ; needed or point moves: why? - (if proof-x-symbol-initialized - (progn - ;; Buffers which have XS minor mode toggled always keep - ;; x-symbol-language set. - (setq x-symbol-language proof-assistant-symbol) - (if (eq x-symbol-mode (not proof-x-symbol-enable)) - ;; toggle x-symbol-mode - (x-symbol-mode)) - ;; Font lock mode must be engaged for x-symbol to do its job - ;; properly, at least when there is no mule around. - (if (and x-symbol-mode (not (featurep 'mule))) - (if (not font-lock-mode) - (font-lock-mode) - ;; Even if font-lock was on before we may need - ;; to refontify now that the patterns (and buffer - ;; contents) have changed. I think x-symbol - ;; ought to do this really! - (font-lock-fontify-buffer))))))) -(defun proof-x-symbol-configure () - "Configure the current buffer for X-Symbol." - (if proof-x-symbol-enable - (progn - (setq x-symbol-language proof-assistant-symbol) - (proof-x-symbol-decode-region (point-min) (point-max))) - (setq x-symbol-language nil))) + (defun proof-x-symbol-mode-all-buffers () "Activate/deactivate x-symbols in all Proof General buffers. A subroutine of proof-x-symbol-enable." - ;; Shell has its own routine + ;; Shell has its own configuration (proof-with-current-buffer-if-exists proof-shell-buffer (proof-x-symbol-shell-config)) ;; Response and goals buffer are fontified/decoded - ;; manually in the code. + ;; manually in the code, configuration only sets + ;; x-symbol-language. (proof-with-current-buffer-if-exists proof-goals-buffer - (proof-x-symbol-configure) - (proof-fontify-buffer)) + (proof-x-symbol-configure)) (proof-with-current-buffer-if-exists proof-response-buffer - (proof-x-symbol-configure) - (proof-fontify-buffer)) + (proof-x-symbol-configure)) ;; Script buffers are in x-symbol mode (let ((bufs (proof-buffers-in-mode proof-mode-for-script))) @@ -217,20 +188,53 @@ A subroutine of proof-x-symbol-enable." (with-current-buffer (car bufs) (proof-x-symbol-mode)) (setq bufs (cdr bufs))))) +;; Three functions for configuring buffers: +;; +;; proof-x-symbol-configure: for goals/response buffer +;; proof-x-symbol-shell-config: for shell buffer (input hook) +;; + + +;; ###autoload +(defun proof-x-symbol-configure () + "Configure the current buffer (goals or response) for X-Symbol." + (if proof-x-symbol-enable + (progn + (setq x-symbol-language proof-assistant-symbol) + ;; If we're turning on x-symbol, attempt to convert to + ;; characters. (Only works if the buffer already + ;; contains tokens!) + (x-symbol-decode)))) + ;; Encoding back to tokens doesn't work too well: needs to + ;; do some de-fontification to remove font properties, and + ;; is flaky anyway because token -> char not nec injective. + ; (if (boundp 'x-symbol-language) + ; ;; If we're turning off x-symbol, convert back to tokens. + ; (x-symbol-encode)))) ;; #### autoload (defun proof-x-symbol-shell-config () "Configure the proof shell for x-symbol, if proof-x-symbol-support<>nil. Assumes that the current buffer is the proof shell buffer." + ;; The best strategy seems to be *not* to turn on decoding + ;; in the shell itself. The reason is that there can be + ;; a clash between annotations and X-Symbol characters + ;; which leads to funny effects later. Moreover, the + ;; user isn't encouraged to interact directly with the + ;; shell, so we don't need to be helpful there. + ;; So we keep the shell buffer as plain text plus annotations. + ;; Even font-lock is problematical, so it should be switched off + ;; too. (if proof-x-symbol-initialized (progn (cond (proof-x-symbol-enable + (setq x-symbol-language proof-assistant-symbol) (if (and proof-xsym-activate-command (proof-shell-live-buffer)) (proof-shell-invisible-command proof-xsym-activate-command 'wait)) - ;; Do the encoding as the first step of input manipulation + ;; We do encoding as the first step of input manipulation (add-hook 'proof-shell-insert-hook 'proof-x-symbol-encode-shell-input)) ((not proof-x-symbol-enable) @@ -240,10 +244,34 @@ Assumes that the current buffer is the proof shell buffer." proof-xsym-deactivate-command 'wait)) (remove-hook 'proof-shell-insert-hook 'proof-x-symbol-encode-shell-input) + ;; NB: x-symbol automatically adds an output filter but + ;; it doesn't actually get used unless the minor mode is + ;; active. Removing it here is just tidying up. (remove-hook 'comint-output-filter-functions - 'x-symbol-comint-output-filter))) - ;; switch the mode on/off in the buffer - (proof-x-symbol-mode)))) + 'x-symbol-comint-output-filter)))))) + +;; ### autoload +(defun proof-x-symbol-mode () + "Turn on/off x-symbol mode in current buffer, from proof-x-symbol-enable. +The X-Symbol minor mode is only useful in script buffers." + (interactive) + (save-excursion ; needed or point moves: why? + (if proof-x-symbol-initialized + (progn + ;; Buffers which have XS minor mode toggled always keep + ;; x-symbol-language set. + (setq x-symbol-language proof-assistant-symbol) + (x-symbol-mode (if proof-x-symbol-enable 1 0)) + ;; Font lock mode must be engaged for x-symbol to do its job + ;; properly, at least when there is no mule around. + (if (and x-symbol-mode (not (featurep 'mule))) + (if (not font-lock-mode) + (font-lock-mode) + ;; Even if font-lock was on before we may need to + ;; refontify now that the patterns (and buffer + ;; contents) have changed. Shouldn't x-symbol do this? + (font-lock-fontify-buffer))))))) + diff --git a/generic/proof.el b/generic/proof.el index 21a8e6bc..21b17b7f 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -273,7 +273,10 @@ Returns new END value." (narrow-to-region start end) (if proof-output-fontify-enable (let ((font-lock-keywords proof-font-lock-defaults)) + ; fontify-region doesn't work for FSF Emacs 20.4, sigh. (font-lock-fontify-region start end) + ; has annoying messages + ; (font-lock-fontify-buffer) ; hope okay cos narrow region. ;; FIXME: this should be optional, really. (proof-zap-commas-region start end))) (if proof-shell-leave-annotations-in-output @@ -283,7 +286,7 @@ Returns new END value." (goto-char start) (while (< (point) (point-max)) (forward-char) - (unless (< (char-to-int (char-before (point))) 128) + (unless (< (char-before (point)) 128) ; char-to-int in XEmacs (delete-char -1))) (goto-char p))) (proof-x-symbol-decode-region start (point-max)) @@ -304,34 +307,31 @@ 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." + (if (string-equal str "\n") + str ; quick exit, no display. (let (start end) (with-current-buffer proof-response-buffer ;; da: I've moved newline before the string itself, to match ;; the other cases when messages are inserted and to cope ;; with warnings after delayed output (non newline terminated). + ; (ugit (format "End is %i" (point-max))) (goto-char (point-max)) (newline) (setq start (point)) - (insert str) + (insert str) + (unless (bolp) (newline)) (setq end (proof-fontify-region start (point))) - ;; This is why we can't keep the buffer in font-lock - ;; minor mode: it destroys this hacky property as soon - ;; as it's made! + ;; This is one reason why we don't keep the buffer in font-lock + ;; minor mode: it destroys this hacky property as soon as it's + ;; made! (Using the minor mode is much more convenient, tho') (if face (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))))) - -;; FIXME da: this window dedicated stuff is a real pain and I've -;; spent ages inserting workarounds. Why do we want it?? -;; The latest problem is that with -;; (setq special-display-regexps -;; (cons "\\*Inferior .*-\\(goals\\|response\\)\\*" -;; special-display-regexps)) -;; I get the script buffer made into a dedicated buffer, -;; presumably because the wrong window is selected below? + (buffer-substring start (point-max)))))) (defun proof-display-and-keep-buffer (buffer &optional pos) "Display BUFFER and mark window according to `proof-window-dedicated'. |