diff options
-rw-r--r-- | generic/pg-goals.el | 22 | ||||
-rw-r--r-- | generic/pg-response.el | 26 | ||||
-rw-r--r-- | generic/proof-shell.el | 61 |
3 files changed, 68 insertions, 41 deletions
diff --git a/generic/pg-goals.el b/generic/pg-goals.el index 55a64bfc..ecb5ce74 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.el @@ -73,23 +73,25 @@ May enable proof-by-pointing or similar features. ;; ;; Goals buffer processing ;; -(defun pg-goals-display (string) +(defun pg-goals-display (string keepresponse) "Display STRING in the `proof-goals-buffer', properly marked up. -Converts term substructure markup into mouse-highlighted extents." +Converts term substructure markup into mouse-highlighted extents. + +The response buffer may be cleared to avoid confusing the user +with output associated with a previous goals message. This +function tries to do that by calling `pg-response-maybe-erase'. + +If KEEPRESPONSE is non-nil, we assume that a response message +corresponding to this goals message has already been displayed +before this goals message (see `proof-shell-handle-delayed-output'), +so the response buffer should not be cleared." (save-excursion ;; Response buffer may be out of date. It may contain (error) ;; messages relating to earlier proof states - ;; NB: this isn't always the case. In Isabelle - ;; we get <WARNING MESSAGE> <CURRENT GOALS> output, - ;; or <WARNING MESSAGE> <ORDINARY MESSAGE>. Both times - ;; <WARNING MESSAGE> would be relevant. - ;; We should only clear the output that was displayed from - ;; the *previous* prompt. - ;; Erase the response buffer if need be, maybe removing the ;; window. Indicate it should be erased before the next output. - (pg-response-maybe-erase t t) + (pg-response-maybe-erase t t nil keepresponse) ;; Erase the goals buffer and add in the new string (set-buffer proof-goals-buffer) diff --git a/generic/pg-response.el b/generic/pg-response.el index a24376b8..6ee58713 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -219,14 +219,27 @@ For multiple frame mode, this function obeys the setting of ;;;###autoload (defun pg-response-maybe-erase - (&optional erase-next-time clean-windows force) - "Erase the response buffer according to `pg-response-erase-flag'. + (&optional erase-next-time clean-windows force keep) + "Erase the response buffer, according to confusing flag combinations. + +Mainly, we look at `pg-response-erase-flag' and clear the +response buffer if this is non-nil, but NOT the special +symbol 'invisible. + ERASE-NEXT-TIME is the new value for the flag. -If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing. -If FORCE, override `pg-response-erase-flag'. -If the user option `proof-tidy-response' is nil, then -the buffer is only cleared when FORCE is set. +FORCE overrides the flag to force cleaning. + +KEEP overrides the flag to prevent cleaning. + +FORCE takes precedent over KEEP. + +If CLEAN-WINDOWS is set, use `proof-clean-buffer' to do the erasing, +otherwise we use `bufhist-checkpoint-and-erase' to record an +undo history entry for the current buffer contents. + +If the user option `proof-tidy-response' is nil, the buffer +will never be cleared unless FORCE is set. No effect if there is no response buffer currently. Returns non-nil if response buffer was cleared." @@ -234,6 +247,7 @@ Returns non-nil if response buffer was cleared." (let ((inhibit-read-only t) (doit (or (and proof-tidy-response + (not keep) (not (eq pg-response-erase-flag 'invisible)) pg-response-erase-flag) force))) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 9cdce998..c889b789 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1472,43 +1472,49 @@ by the filter is to send the next command from the queue." (pg-response-display str))) (defun proof-shell-handle-delayed-output () - "Display delayed outputs, when queue is stopped or completed. + "Display delayed goals/responses, when queue is stopped or completed. This function handles the cases of `proof-shell-output-kind' which are not dealt with eagerly during script processing, namely 'response and 'goals types. -This is useful even with empty delayed output as it can -clear the buffers. +This is useful even with empty delayed output as it will empty +the buffers. The delayed output is in the region \[proof-shell-delayed-output-start,proof-shell-delayed-output-end]. +If no goals classified output is found, the whole output is +displayed in the response buffer. + If goals output is found, the last matching instance, possibly -bounded by `proof-shell-end-goals-regexp', will be displayed. -Any output that appears *before* the first goals output (but +bounded by `proof-shell-end-goals-regexp', will be displayed +in the goals buffer (and may be further analysed by Proof General). + +Any output that appears *before* the last goals output (but after messages classified as urgent, see `proof-shell-filter') -will also be displayed in the response buffer. For example, -if OUTPUT has this form: +will also be displayed in the response buffer. + +For example, if OUTPUT has this form: MESSSAGE-1 GOALS-1 MESSAGE-2 GOALS-2 + JUNK then GOALS-2 will be displayed in the goals buffer, and MESSAGE-2 -in the response buffer. Notice that the above alternation can +in the response buffer. JUNK will be ignored. + +Notice that the above alternation (and separation of JUNK) can 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. +and `proof-shell-end-goals-regexp' are set. With just the start +goals regexp set, GOALS-2 JUNK will appear in the goals buffer +and no response output would occur. The goals and response outputs are copied into `proof-shell-last-goals-output' and `proof-shell-last-response-output' respectively. -If no other kind of classified output is found, the default -is to display the output in the response buffer. - The value returned is the value for `proof-shell-last-output-kind', i.e., 'goals or 'response." (let ((start proof-shell-delayed-output-start) @@ -1522,8 +1528,9 @@ i.e., 'goals or 'response." (gstart (or (match-end 1) ; start of actual display gmark)) (rstart start) ; possible response before goals - (gend end)) - ;; Find the last goal string in the output + (gend end) + both) ; flag for response+goals + (goto-char gstart) (while (re-search-forward proof-shell-start-goals-regexp end t) (setq gmark (match-beginning 0)) @@ -1537,19 +1544,23 @@ i.e., 'goals or 'response." end))) (setq proof-shell-last-goals-output (buffer-substring-no-properties gstart gend)) + + ;; FIXME heuristic: 4 allows for annotation in end-goals-regexp [is it needed?] + (setq both + (> (- gmark rstart) 4)) + (if both + (proof-shell-display-output-as-response + flags + (buffer-substring-no-properties rstart gmark))) + ;; display goals output second so it persists in 2-pane mode (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 (> (- gmark rstart) 4) - (proof-shell-display-output-as-response - flags - (buffer-substring-no-properties rstart gmark))) - ;; primary output kind is goals + (pg-goals-display proof-shell-last-goals-output both)) + ;; indicate a goals output has been given 'goals)) - (t ; Any unclassified output will appear as a response. + (t (proof-shell-display-output-as-response flags proof-shell-last-output) + ;; indicate that (only) a response output has been given 'response)) (run-hooks 'proof-shell-handle-delayed-output-hook))) |