From cee50def1d068fdff8881c0c98718a3f50047035 Mon Sep 17 00:00:00 2001 From: David Aspinall Date: Tue, 10 Jan 2012 13:10:25 +0000 Subject: Tweak message and display model, in particular, make sure that when a response appears above a goals output, the goals output is displayed second, so it is the one that remains visible to the user in the default 2-pane mode. This works with output like this in HOL Light: Warning: Free variables in goal: A, B val it : goalstack = 1 subgoal (1 total) ... and similar cases in Isabelle and Coq. The fix involves some ugly messing with the flags for clearing the response buffer (see `pg-response-maybe-erase'). This could surely be streamlined. --- generic/proof-shell.el | 61 +++++++++++++++++++++++++++++--------------------- 1 file changed, 36 insertions(+), 25 deletions(-) (limited to 'generic/proof-shell.el') 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))) -- cgit v1.2.3