diff options
| -rw-r--r-- | generic/pg-goals.el | 88 | ||||
| -rw-r--r-- | generic/pg-response.el | 113 | ||||
| -rw-r--r-- | generic/proof-shell.el | 130 |
3 files changed, 131 insertions, 200 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index f3ac36df..8d854ce3 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -8,12 +8,18 @@ ;; $Id$ ;; +;; A sub-module of proof-shell; assumes proof-script loaded. + +(require 'pg-assoc) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Goals buffer mode ;; -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; The mode itself +;; (eval-and-compile ; to define proof-goals-mode-map (define-derived-mode proof-goals-mode proof-universal-keys-only-mode proof-general-name @@ -56,6 +62,10 @@ May enable proof-by-pointing or similar features. "Menu for Proof General goals buffer." proof-aux-menu) + +;; +;; The completion of init +;; (defun proof-goals-config-done () "Initialise the goals buffer after the child has been configured." (proof-font-lock-configure-defaults nil) @@ -235,12 +245,12 @@ commands which can be sent to the prover." ;; Finally: strip the specials. This should ;; leave the spans in exactly the right place. - (pg-goals-strip-subterm-markup-buf start end)))) + (pg-assoc-strip-subterm-markup-buf start end)))) (defun pg-goals-make-top-span (start end) "Make a top span (goal/hyp area) for mouse active output." - (let (span name) + (let (span typname) (goto-char start) ;; skip the pg-topterm-char itself (forward-char) @@ -258,78 +268,6 @@ commands which can be sent to the prover." (set-span-property span 'proof-top-element typname))) -(defun pg-goals-strip-subterm-markup (string) - "Return STRING with subterm and pbp annotations removed. -Special annotations are characters with codes higher than -'pg-subterm-first-special-char'. -If pg-subterm-first-special-char is unset, return STRING unchanged." - (if pg-subterm-first-special-char - (let* ((ip 0) (op 0) (l (length string)) (out (make-string l ?x ))) - (while (< ip l) - (if (>= (aref string ip) pg-subterm-first-special-char) - (if (char-equal (aref string ip) pg-subterm-start-char) - (progn (incf ip) - ;; da: this relies on annotations being - ;; characters between \200 and first special - ;; char (e.g. \360). Why not just look for - ;; the sep char?? - (while - (< (aref string ip) - pg-subterm-first-special-char) - (incf ip)))) - (aset out op (aref string ip)) - (incf op)) - (incf ip)) - (substring out 0 op)) - string)) - -(defun pg-goals-strip-subterm-markup-buf (start end) - "Remove subterm and pbp annotations from region." - ;; FIXME: create these regexps ahead of time. - (if pg-subterm-start-char - (let ((ann-regexp - (concat - (regexp-quote (char-to-string pg-subterm-start-char)) - "[^" - (regexp-quote (char-to-string pg-subterm-sep-char)) - "]*" - (regexp-quote (char-to-string pg-subterm-sep-char))))) - (save-restriction - (narrow-to-region start end) - (goto-char start) - (proof-replace-regexp ann-regexp "") - (goto-char start) - (proof-replace-string (char-to-string pg-subterm-end-char) "") - (goto-char start) - (if pg-topterm-char - (proof-replace-string (char-to-string pg-topterm-char) "")))))) - - - -(defun pg-goals-strip-subterm-markup-buf-old (start end) - "Remove subterm and pbp annotations from region." - (let (c) - (goto-char start) - (while (< (point) end) - ;; FIXME: small OBO here: if char at end is special - ;; it won't be removed. - (if (>= (setq c (char-after (point))) - pg-subterm-first-special-char) - (progn - (delete-char 1) - (decf end) - (if (char-equal c pg-subterm-start-char) - (progn - ;; FIXME: could simply replace this by replace - ;; match, matching on sep-char?? - (while (and (< (point) end) - (< (char-after (point)) - pg-subterm-first-special-char)) - (delete-char 1) - (decf end))))) - (forward-char))) - end)) - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Commands to prover based on subterm markup (inc PBP). diff --git a/generic/pg-response.el b/generic/pg-response.el index 65fe9343..2d2a46ba 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -8,6 +8,9 @@ ;; $Id$ ;; +;; A sub-module of proof-shell; assumes proof-script loaded. +(require 'pg-assoc) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Response buffer mode @@ -15,14 +18,6 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (eval-and-compile -(define-derived-mode proof-universal-keys-only-mode fundamental-mode - proof-general-name "Universal keymaps only" - ;; Doesn't seem to supress TAB, RET - (suppress-keymap proof-universal-keys-only-mode-map 'all) - (proof-define-keys proof-universal-keys-only-mode-map - proof-universal-keys))) - -(eval-and-compile (define-derived-mode proof-response-mode proof-universal-keys-only-mode "PGResp" "Responses from Proof Assistant" (setq proof-buffer-type 'response) @@ -30,7 +25,7 @@ (easy-menu-add proof-response-mode-menu proof-response-mode-map) (easy-menu-add proof-assistant-menu proof-response-mode-map) (proof-toolbar-setup) - (setq proof-shell-next-error nil) ; all error msgs lost! + (setq pg-response-next-error nil) ; all error msgs lost! (erase-buffer))) (easy-menu-define proof-response-mode-menu @@ -130,7 +125,7 @@ Returns non-nil if response buffer was cleared." ;; NB: useful optional arg to erase buffer is XEmacs specific, 8-(. ;; (erase-buffer proof-response-buffer) (with-current-buffer proof-response-buffer - (setq proof-shell-next-error nil) ; all error msgs lost! + (setq pg-response-next-error nil) ; all error msgs lost! (erase-buffer)))) (setq pg-response-erase-flag erase-next-time) doit))) @@ -138,7 +133,7 @@ Returns non-nil if response buffer was cleared." (defun pg-response-display (str) "Show STR as a response in the response buffer." (unless pg-use-specials-for-fontify - (setq str (pg-goals-strip-subterm-markup str))) + (setq str (pg-assoc-strip-subterm-markup str))) (proof-shell-maybe-erase-response t nil) (pg-response-display-with-face str) (proof-display-and-keep-buffer proof-response-buffer)) @@ -175,6 +170,99 @@ Returns non-nil if response buffer was cleared." + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; +;; Next error function. +;; + +(defvar pg-response-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 + pg-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 pg-response-next-error 0))) + (and (consp argp) 1) + (or pg-response-next-error 1))) + line column file errpos) + (set-buffer proof-response-buffer) + (goto-char (point-min)) + (if (re-search-forward pg-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 pg-response-next-error wanted-error) + (if (and + pg-next-error-filename-regexp + ;; Look for the most recently mentioned filename + (re-search-backward + pg-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 pg-next-error-extract-filename + (format + pg-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 pg-response-next-error nil) + (error "proof-next-error: couldn't find next error."))))) + + + + + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Tracing buffers @@ -183,7 +271,7 @@ Returns non-nil if response buffer was cleared." ;; An analogue of pg-response-display-with-face (defun proof-trace-buffer-display (str) "Display STR in the trace buffer." - (let (start end) + (let (start) (with-current-buffer proof-trace-buffer (goto-char (point-max)) (newline) @@ -195,5 +283,6 @@ Returns non-nil if response buffer was cleared." + (provide 'pg-response) ;; pg-response.el ends here. 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. |