diff options
Diffstat (limited to 'generic/proof-shell.el')
| -rw-r--r-- | generic/proof-shell.el | 100 |
1 files changed, 52 insertions, 48 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 4749a55b..788d32da 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1,6 +1,6 @@ ;;; proof-shell.el --- Proof General shell mode. ;; -;; Copyright (C) 1994-2009 LFCS Edinburgh. +;; Copyright (C) 1994-2010 LFCS Edinburgh. ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira ;; License: GPL (GNU GENERAL PUBLIC LICENSE) @@ -41,15 +41,16 @@ The value is a list of lists of the form (SPAN COMMANDS ACTION [FLAGS]) -which is the queue of things to do. Flags are set for non-standard -commands (out of script). They may include +which is the queue of things to do. Flags are set for non-scripting +commands or for when scripting should not bother the user. +They may include 'no-response-display do not display messages in *response* buffer 'no-error-display do not display errors/take error action 'no-goals-display do not goals in *goals* buffer If flags are non-empty, other interactive cues will be surpressed. -\(E.g., printing help messages). +\(E.g., printing hints). See the functions `proof-start-queue' and `proof-shell-exec-loop'.") @@ -396,7 +397,7 @@ shell buffer, alled by `proof-shell-bail-out' if process exits." (bufname (buffer-name))) (message "%s, cleaning up and exiting..." bufname) - (let (timeout-id) + (let (timeout-id) (redisplay t) ; redisplay (if alive ; process still there (progn @@ -503,10 +504,11 @@ This simply kills the `proof-shell-buffer' relying on the hook function (error "No proof shell buffer to kill!"))) (defun proof-shell-bail-out (process event) - "Value for the process sentinel for the proof assistant process. -If the proof assistant dies, run proof-shell-kill-function to + "Value for the process sentinel for the proof assistant PROCESS. +If the proof assistant dies, run `proof-shell-kill-function' to cleanup and remove the associated buffers. The shell buffer is -left around so the user may discover what killed the process." +left around so the user may discover what killed the process. +EVENT is the string describing the change." (message "Process %s %s, shutting down scripting..." process event) (proof-shell-kill-function) (message "Process %s %s, shutting down scripting...done." process event)) @@ -605,7 +607,7 @@ non-empty flags) will not invoke any of this action." ; PG4.0 change (unless (memq 'no-error-display flags) (cond ((eq err-or-int 'interrupt) - (pg-response-maybe-erase t t t) ; force cleaned now & next + (pg-response-maybe-erase t t t) ; force cleaned now & next (proof-shell-handle-error-output (if proof-shell-truncate-before-error proof-shell-interrupt-regexp) 'proof-error-face) @@ -626,7 +628,7 @@ non-empty flags) will not invoke any of this action." ; PG4.0 change (unless proof-shell-quiet-errors (beep)) (proof-with-current-buffer-if-exists proof-script-buffer - (proof-script-clear-queue-spans-on-error + (proof-script-clear-queue-spans-on-error (car-safe (car-safe proof-action-list)))) (setq proof-action-list nil) (proof-release-lock) @@ -660,7 +662,7 @@ This is a hook function for proof-shell-handle-delayed-output-hook." "See if the output between START and END must be dealt with immediately. To speed up processing, PG tries to avoid displaying output that the user will not have a chance to see. Some output must be -handled immediately, however: these are errors, interrupts, +handled immediately, however: these are errors, interrupts, goals and loopbacks (proof step hints/proof by pointing results). In this function we check, in turn: @@ -797,7 +799,7 @@ used in `proof-add-to-queue' when we start processing a queue, and in (goto-char (point-max)) ;; TEMP: next step: preprocess list of strings directly - (let ((string (apply 'concat strings))) + (let ((string (apply 'concat strings))) ;; Hook for munging `string' and other dirty hacks. (run-hooks 'proof-shell-insert-hook) @@ -878,7 +880,7 @@ track what happens in the proof queue." Comments are not sent to the prover." (let (cbitems nextitem) (while (and proof-action-list - (not (nth 1 (setq nextitem + (not (nth 1 (setq nextitem (car proof-action-list))))) (setq cbitems (cons nextitem cbitems)) (setq proof-action-list (cdr proof-action-list))) @@ -911,7 +913,7 @@ being processed." ;; (should have proof-action-list<>nil -> busy) (and proof-shell-busy queuemode (unless (eq proof-shell-busy queuemode) - (proof-debug + (proof-debug "proof-append-alist: wrong queuemode detected for busy shell") (assert (eq proof-shell-busy queuemode))))) @@ -1030,9 +1032,9 @@ The return value is non-nil if the action list is now empty." (defun proof-shell-insert-loopback-cmd (cmd) - "Insert command sequence sent from prover into script buffer. + "Insert command string CMD sent from prover into script buffer. String is inserted at the end of locked region, after a newline -and indentation. Assumes proof-script-buffer is active." +and indentation. Assumes `proof-script-buffer' is active." (unless (string-match "^\\s-*$" cmd) ; FIXME: assumes cmd is single line (with-current-buffer proof-script-buffer (let (span) @@ -1088,7 +1090,7 @@ ends with text matching `proof-shell-eager-annotation-end'." (proof-shell-process-urgent-message-elisp)) ((proof-looking-at-safe proof-shell-match-pgip-cmd) - (pg-pgip-process-packet + (pg-pgip-process-packet ;; NB: xml-parse-region ignores junk before XML (xml-parse-region start end))) @@ -1108,11 +1110,11 @@ ends with text matching `proof-shell-eager-annotation-end'." ;; Clear the response buffer this time, but not next, leave window. (pg-response-maybe-erase nil nil) (proof-minibuffer-message - (buffer-substring-no-properties - (save-excursion + (buffer-substring-no-properties + (save-excursion (re-search-forward proof-shell-eager-annotation-start end nil) (point)) - (min end + (min end (save-excursion (end-of-line) (point)) (+ start 75)))) (pg-response-display-with-face @@ -1122,7 +1124,7 @@ ends with text matching `proof-shell-eager-annotation-end'." (defun proof-shell-process-urgent-message-trace (start end) "Display a message in the tracing buffer. A subroutine of `proof-shell-process-urgent-message'." - (proof-trace-buffer-display + (proof-trace-buffer-display (buffer-substring-no-properties start end)) (unless (and proof-trace-output-slow-catchup (pg-tracing-tight-loop)) @@ -1173,7 +1175,7 @@ A subroutine of `proof-shell-process-urgent-message'." (let ((names (match-string 1)) (deps (match-string 2)) (sep proof-shell-theorem-dependency-list-split)) - (setq + (setq proof-last-theorem-dependencies (cons (split-string names sep) (split-string deps sep))))) @@ -1219,7 +1221,7 @@ A subroutine of `proof-shell-process-urgent-message'." "Filter for the proof assistant shell-process. A function for `scomint-output-filter-functions'. -Deal with output and issue new input from the queue. This is +Deal with output STR and issue new input from the queue. This is an important internal function. Handle urgent messages first. As many as possible are processed, @@ -1242,9 +1244,9 @@ example, in this case: `proof-marker' points after INPUT. `proof-shell-urgent-message-marker' points after URGENT-MESSAGE-2, -after both urgent messages have been processed by -`proof-shell-process-urgent-messages'. Urgent messages always -processed; they are intended to correspond to informational +after both urgent messages have been processed by +`proof-shell-process-urgent-messages'. Urgent messages always +processed; they are intended to correspond to informational notes that the prover makes to inform the user or interface on progress. @@ -1302,7 +1304,7 @@ is only changed when input is sent in `proof-shell-insert'." (progn (setq endpos (match-beginning 0)) (setq proof-shell-last-prompt - (buffer-substring-no-properties + (buffer-substring-no-properties endpos (match-end 0))) (goto-char (point-max)) (setq proof-shell-expecting-output nil) @@ -1335,13 +1337,13 @@ messages." "Scan the shell buffer for urgent messages. Scanning starts from `proof-shell-urgent-message-scanner' or `scomint-last-input-end', which ever is later. We deal with strings -between regexps `proof-shell-eager-annotation-start' and -`proof-shell-eager-annotation-end'. +between regexps `proof-shell-eager-annotation-start' and +`proof-shell-eager-annotation-end'. We update `proof-shell-urgent-message-marker' to point to last message found. This is a subroutine of `proof-shell-filter'." - (let ((pt (point)) (end t) + (let ((pt (point)) (end t) lastend laststart (initstart (max (marker-position proof-shell-urgent-message-scanner) (marker-position scomint-last-input-end)))) @@ -1357,11 +1359,11 @@ This is a subroutine of `proof-shell-filter'." ;; Process the region including the annotations (proof-shell-process-urgent-message laststart lastend)))) - (set-marker + (set-marker proof-shell-urgent-message-scanner (if end ;; couldn't find message start; move forward to avoid rescanning (max initstart - (- (point) + (- (point) (1+ proof-shell-eager-annotation-start-length))) ;; incomplete message; leave marker at start of message laststart)) @@ -1398,7 +1400,7 @@ by the filter is to send the next command from the queue." ;; Keep a copy of the last message from the prover ;; PG 4.0: this is kept verbatim, never modified. - (setq proof-shell-last-output + (setq proof-shell-last-output (buffer-substring-no-properties start end)) ;; sets proof-shell-last-output-kind @@ -1429,7 +1431,7 @@ are not dealt with eagerly during script processing, namely This is useful even with empty delayed output as it can clear the buffers. -The delayed output is in the region +The delayed output is in the region \[proof-shell-last-output-start,proof-shell-last-output-end]. If goals output is found, the last matching instance, possibly @@ -1446,7 +1448,7 @@ if OUTPUT has this form: then GOALS-2 will be displayed in the goals buffer, and MESSAGE-2 in the response buffer. Notice that the above alternation can -only be distinguished if both `proof-shell-start-goals-regexp' +only be distinguished if both `proof-shell-start-goals-regexp' and `proof-shell-end-goals-regexp' are set. With just the former, MESSAGE-1 GOALS-1 MESSAGE-2 would all appear in the response buffer. @@ -1471,22 +1473,22 @@ i.e., 'goals or 'response." (goto-char gstart) (while (re-search-forward proof-shell-start-goals-regexp end t) (setq gstart (match-beginning 0)) - (setq gend + (setq gend (if proof-shell-end-goals-regexp (progn (re-search-forward proof-shell-end-goals-regexp end t) (match-beginning 0) (setq rstart (match-end 0))) end))) - (setq proof-shell-last-goals-output + (setq proof-shell-last-goals-output (buffer-substring-no-properties gstart gend)) (unless (memq 'no-goals-display flags) (pg-goals-display proof-shell-last-goals-output)) ;; also allow (for Coq) any preceding output as a response ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp (when (> (- gstart rstart) 4) - (proof-shell-display-output-as-response - flags + (proof-shell-display-output-as-response + flags (buffer-substring-no-properties rstart gstart))) ;; primary output kind is goals 'goals)) @@ -1587,15 +1589,17 @@ Only works when system timer has microsecond count available." ;; ;;;###autoload -(defun proof-shell-wait () +(defun proof-shell-wait (&optional interrupt-on-input) "Busy wait for `proof-shell-busy' to become nil. Needed between sequences of commands to maintain synchronization, because Proof General does not allow for the action list to be extended in some cases. May be called by `proof-shell-invisible-command'." (let ((proverproc (get-buffer-process proof-shell-buffer))) (when proverproc - (while (and proof-shell-busy (not quit-flag)) - (accept-process-output proverproc 1) + (while (and proof-shell-busy (not quit-flag) + (or (not interrupt-on-input) (input-pending-p))) + (accept-process-output proverproc 0.2) ;; NB: FIXME likely GE 23-ism + ;; assume filters ran, redisplay (redisplay t)) (if quit-flag (error "Proof General: Quit in proof-shell-wait"))))) @@ -1612,7 +1616,7 @@ Calls proof-state-change-hook." The CMD is `invisible' in the sense that it is not recorded in buffer. CMD may be a string or a string-yielding expression. -Automatically add proof-terminal-char if necessary, examining +Automatically add `proof-terminal-char' if necessary, examining `proof-shell-no-auto-terminate-commands'. By default, let the command be processed asynchronously. @@ -1625,7 +1629,7 @@ INVISIBLECALLBACK will be invoked after the command has finished, if it is set. It should probably run the hook variables `proof-state-change-hook'. -If NOERROR is set, surpress usual error action." +FLAGS are put onto the If NOERROR is set, surpress usual error action." (unless (stringp cmd) (setq cmd (eval cmd))) (if cmd @@ -1715,16 +1719,16 @@ Error messages are displayed as usual." ;; scomint customisation. - (setq scomint-output-filter-functions + (setq scomint-output-filter-functions (append (if proof-shell-strip-crs-from-output 'scomint-strip-ctrl-m) (list 'proof-shell-filter))) (setq proof-marker ; follows prompt - (make-marker) - proof-shell-urgent-message-marker + (make-marker) + proof-shell-urgent-message-marker (make-marker) ; follows urgent messages - proof-shell-urgent-message-scanner + proof-shell-urgent-message-scanner (make-marker)) ; last scan point (set-marker proof-shell-urgent-message-scanner (point-min)) |