Hi,
here is a patch that solves the problem for me. Any comments?
Bye,
Hendrik
Index: generic/proof-shell.el
===================================================================
RCS file: /disk/cvs/proofgen/ProofGeneral/generic/proof-shell.el,v
retrieving revision 12.15
diff -u -r12.15 proof-shell.el
--- generic/proof-shell.el 3 Jan 2013 09:33:38 -0000 12.15
+++ generic/proof-shell.el 9 Jan 2013 20:49:38 -0000
@@ -243,6 +243,13 @@
: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 @@
(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,37 @@
;; The proof shell process filter
;;
+(defun proof-shell-filter-wrapper (str)
+ "Wrapper for `proof-shell-filter', protecting against recursive 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 recursive 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 str)
+ (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 (str)
"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 STR and issue new input from the queue. This is
+an important internal function. Actually, STR is not used, the
+output is taken from `proof-shell-buffer'.
Handle urgent messages first. As many as possible are processed,
using the function `proof-shell-process-urgent-messages'.
@@ -1806,7 +1839,7 @@
(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)
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
