diff options
| -rw-r--r-- | doc/PG-adapting.texi | 36 | ||||
| -rw-r--r-- | generic/proof-shell.el | 54 |
2 files changed, 80 insertions, 10 deletions
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 4969b5db..1684e882 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -4229,15 +4229,25 @@ ends with text matching @samp{@code{proof-shell-eager-annotation-end}}. @end defun The main processing point which triggers other actions is -@code{proof-shell-filter}. +@code{proof-shell-filter}. It is called from +@code{proof-shell-filter-wrapper}, which itself is called from an +ordinary Emacs process filter inside the simplified @code{comint} +library that is distributed with Proof General (in +@code{lib/scomint.el}). @c TEXI DOCSTRING MAGIC: proof-shell-filter -@defun proof-shell-filter str +@defun proof-shell-filter Master filter for the proof assistant shell-process.@* A function for @samp{@code{scomint-output-filter-functions}}. -Deal with output @var{str} and issue new input from the queue. This is -an important internal function. +Deal with output and issue new input from the queue. This is an +important internal function. The output must be collected from +@samp{@code{proof-shell-buffer}} for the following reason. This function +might block inside @samp{@code{process-send-string}} when sending input to +the proof assistant or to prooftree. In this case Emacs might +call the process filter again while the previous instance is +still running. @samp{@code{proof-shell-filter-wrapper}} detects and delays +such calls but does not buffer the output. Handle urgent messages first. As many as possible are processed, using the function @samp{@code{proof-shell-process-urgent-messages}}. @@ -4295,8 +4305,22 @@ After processing the current output, the last step undertaken by the filter is to send the next command from the queue. @end defun - - +@c TEXI DOCSTRING MAGIC: proof-shell-filter-wrapper +@defun proof-shell-filter-wrapper str-do-not-use +Wrapper for @samp{@code{proof-shell-filter}}, protecting against parallel calls.@* +In Emacs a process filter function can be called while the same +filter is currently running for the same process, for instance, +when the filter bocks on I/O. This wrapper protects the main +entry point, @samp{@code{proof-shell-filter}} against such parallel, +overlapping calls. + +The argument @var{str-do-not-use} contains the most recent output, but +is discarded. @samp{@code{proof-shell-filter}} collects the output from +@samp{@code{proof-shell-buffer}} (where it is inserted by +@samp{@code{scomint-output-filter}}), relieving this function from the task +to buffer the output that arrives during parallel, overlapping +calls. +@end defun diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 6bfbef51..c304f61d 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -243,6 +243,13 @@ If QUEUEMODE is supplied, set the lock to that value." :type 'boolean :group 'proof-shell) +(defvar proof-shell-filter-active nil + "t when `proof-shell-filter' is running.") + +(defvar proof-shell-filter-was-blocked nil + "t when a recursive call of `proof-shell-filter' was blocked. +In this case `proof-shell-filter' must be called again after it finished.") + (defun proof-shell-set-text-representation () "Adjust representation for current buffer, to match `proof-shell-unicode'." (unless proof-shell-unicode @@ -277,6 +284,7 @@ process command." (interactive) (unless (proof-shell-live-buffer) + (setq proof-shell-filter-active nil) (setq proof-included-files-list nil) ; clear some state (let ((name (buffer-file-name (current-buffer)))) @@ -1288,12 +1296,50 @@ inverse to `proof-register-possibly-new-processed-file'." ;; The proof shell process filter ;; -(defun proof-shell-filter (str) +(defun proof-shell-filter-wrapper (str-do-not-use) + "Wrapper for `proof-shell-filter', protecting against parallel calls. +In Emacs a process filter function can be called while the same +filter is currently running for the same process, for instance, +when the filter bocks on I/O. This wrapper protects the main +entry point, `proof-shell-filter' against such parallel, +overlapping calls. + +The argument STR-DO-NOT-USE contains the most recent output, but +is discarded. `proof-shell-filter' collects the output from +`proof-shell-buffer' (where it is inserted by +`scomint-output-filter'), relieving this function from the task +to buffer the output that arrives during parallel, overlapping +calls." + (if proof-shell-filter-active + (progn + (setq proof-shell-filter-was-blocked t)) + (let ((call-proof-shell-filter t)) + (while call-proof-shell-filter + (setq proof-shell-filter-active t + proof-shell-filter-was-blocked nil) + (condition-case err + (progn + (proof-shell-filter) + (setq proof-shell-filter-active nil)) + ((error quit) + (setq proof-shell-filter-active nil + proof-shell-filter-was-blocked nil) + (signal (car err) (cdr err)))) + (setq call-proof-shell-filter proof-shell-filter-was-blocked))))) + + +(defun proof-shell-filter () "Master filter for the proof assistant shell-process. A function for `scomint-output-filter-functions'. -Deal with output STR and issue new input from the queue. This is -an important internal function. +Deal with output and issue new input from the queue. This is an +important internal function. The output must be collected from +`proof-shell-buffer' for the following reason. This function +might block inside `process-send-string' when sending input to +the proof assistant or to prooftree. In this case Emacs might +call the process filter again while the previous instance is +still running. `proof-shell-filter-wrapper' detects and delays +such calls but does not buffer the output. Handle urgent messages first. As many as possible are processed, using the function `proof-shell-process-urgent-messages'. @@ -1806,7 +1852,7 @@ Error messages are displayed as usual." (setq scomint-output-filter-functions (append (if proof-shell-strip-crs-from-output 'scomint-strip-ctrl-m) - (list 'proof-shell-filter))) + (list 'proof-shell-filter-wrapper))) (setq proof-marker ; follows prompt (make-marker) |