From 58da4a61d5cbb998710e85b8bb5e2911ce6cdec2 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Thu, 15 Aug 2002 23:38:27 +0000 Subject: Refactoring. --- generic/proof-shell.el | 130 +++++++------------------------------------------ 1 file changed, 17 insertions(+), 113 deletions(-) (limited to 'generic/proof-shell.el') diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 30d1a68a..35f3d0f3 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -519,10 +519,21 @@ object files, used by Lego and Coq)." - +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Response buffer processing ;; + +(defvar proof-shell-no-response-display nil + "A setting to disable displays in the response buffer.") + +(defvar proof-shell-urgent-message-marker nil + "Marker in proof shell buffer pointing to end of last urgent message.") + +(defvar proof-shell-urgent-message-scanner nil + "Marker in proof shell buffer pointing to scan start for urgent messages.") + + (defun proof-shell-handle-output (start-regexp end-regexp append-face) "Displays output from `proof-shell-buffer' in `proof-response-buffer'. The region in `proof-shell-buffer begins with the first match @@ -554,7 +565,7 @@ This is a subroutine of proof-shell-handle-error." (setq string (if pg-use-specials-for-fontify (buffer-substring start end) - (pg-goals-strip-subterm-markup + (pg-assoc-strip-subterm-markup (buffer-substring start end))))) ;; Erase if need be, and erase next time round too. (proof-shell-maybe-erase-response t nil) @@ -706,7 +717,7 @@ which see." ((proof-shell-string-match-safe proof-shell-error-regexp string) ;; FIXME: is the next setting correct or even needed? (setq proof-shell-last-output - (pg-goals-strip-subterm-markup + (pg-assoc-strip-subterm-markup (substring string (match-beginning 0)))) (setq proof-shell-last-output-kind 'error)) @@ -742,7 +753,7 @@ which see." pg-subterm-first-special-char (not (string-equal proof-shell-start-goals-regexp - (pg-goals-strip-subterm-markup + (pg-assoc-strip-subterm-markup proof-shell-start-goals-regexp)))) (setq start (match-beginning 0))) (setq end (if proof-shell-end-goals-regexp @@ -1231,7 +1242,7 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end." (proof-trace-buffer-display (if pg-use-specials-for-fontify message - (pg-goals-strip-subterm-markup message))) + (pg-assoc-strip-subterm-markup message))) (proof-display-and-keep-buffer proof-trace-buffer) ;; Force redisplay in case in a fast loop which keeps Emacs ;; fully-occupied processing prover output @@ -1249,8 +1260,7 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end." ;; Don't bother remove the window for the response buffer ;; because we're about to put a message in it. (proof-shell-maybe-erase-response nil nil) - (let ((stripped (pg-goals-strip-subterm-markup message)) - firstline) + (let ((stripped (pg-assoc-strip-subterm-markup message))) ;; Display first chunk of output in minibuffer. ;; Maybe this should be configurable, it can get noisy. (proof-shell-message @@ -1262,15 +1272,6 @@ proof-shell-eager-annotation-start, proof-shell-eager-annotation-end." stripped) 'proof-eager-annotation-face))))) -(defvar proof-shell-no-response-display nil - "A setting to disable displays in the response buffer.") - -(defvar proof-shell-urgent-message-marker nil - "Marker in proof shell buffer pointing to end of last urgent message.") - -(defvar proof-shell-urgent-message-scanner nil - "Marker in proof shell buffer pointing to scan start for urgent messages.") - (defun proof-shell-process-urgent-messages () "Scan the shell buffer for urgent messages. Scanning starts from proof-shell-urgent-message-scanner and handles @@ -1680,15 +1681,12 @@ usual, unless NOERROR is non-nil." ;; Proof General shell mode definition ;; - (eval-and-compile ; to define vars ;;; NB: autoload tag below doesn't work for d-d-m, autoload is in proof.el ;;;###autoload (define-derived-mode proof-shell-mode comint-mode "proof-shell" "Proof General shell mode class for proof assistant processes" - - (setq proof-buffer-type 'shell) ;; Clear state @@ -1802,99 +1800,5 @@ processing." (proof-x-symbol-shell-config)))))) - - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; -;; Next error function. -;; - -(defvar proof-shell-next-error nil - "Error counter in response buffer to count for next error message.") - -;;;###autoload -(defun proof-next-error (&optional argp) - "Jump to location of next error reported in the response buffer. - -A prefix arg specifies how many error messages to move; -negative means move back to previous error messages. -Just C-u as a prefix means reparse the error message buffer -and start at the first error." - (interactive "P") - (if (and ;; At least one setting must be configured - proof-shell-next-error-regexp - ;; Response buffer must be live - (or - (buffer-live-p proof-response-buffer) - (error "proof-next-error: no response buffer to parse!"))) - (let ((wanted-error (or (and (not (consp argp)) - (+ (prefix-numeric-value argp) - (or proof-shell-next-error 0))) - (and (consp arg) 1) - (or proof-shell-next-error 1))) - line column file errpos) - (set-buffer proof-response-buffer) - (goto-char (point-min)) - (if (re-search-forward proof-shell-next-error-regexp - nil t wanted-error) - (progn - (setq errpos (save-excursion - (goto-char (match-beginning 0)) - (beginning-of-line) - (point))) - (setq line (match-string 2)) ; may be unset - (if line (setq line (string-to-int line))) - (setq column (match-string 3)) ; may be unset - (if column (setq column (string-to-int column))) - (setq proof-shell-next-error wanted-error) - (if (and - proof-shell-next-error-filename-regexp - ;; Look for the most recently mentioned filename - (re-search-backward - proof-shell-next-error-filename-regexp nil t)) - (setq file - (if (file-exists-p (match-string 2)) - (match-string 2) - ;; May need post-processing to extract filename - (if proof-shell-next-error-extract-filename - (format - proof-shell-next-error-extract-filename - (match-string 2)))))) - ;; Now find the other buffer we need to display - (let* - ((errbuf - (if file - (find-file-noselect file) - (or proof-script-buffer - ;; We could make more guesses here, - ;; e.g. last script buffer active - ;; (keep a record of it?) - (error - "proof-next-error: can't guess file for error message")))) - (pop-up-windows t) - (rebufwindow - (or (get-buffer-window proof-response-buffer 'visible) - ;; Pop up a window. - (display-buffer proof-response-buffer)))) - ;; Make sure the response buffer stays where it is, - ;; and make sure source buffer is visible - (select-window rebufwindow) - (pop-to-buffer errbuf) - ;; Display the error message in the response buffer - (set-window-point rebufwindow errpos) - (set-window-start rebufwindow errpos) - ;; Find the error location in the error buffer - (set-buffer errbuf) - ;; FIXME: no handling of selective display here - (goto-line line) - (if (and column (> column 1)) - (move-to-column (1- column))))) - (setq proof-shell-next-error nil) - (error "proof-next-error: couldn't find next error."))))) - - - - (provide 'proof-shell) ;; proof-shell.el ends here. -- cgit v1.2.3