here is a patch that solves the problem for me. Any comments?



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 @@
   (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
         (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
ProofGeneral-devel mailing list

Reply via email to