diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2011-10-17 11:10:30 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2011-10-17 11:10:30 +0000 |
commit | 2218f6c7b27e09623fcb7f94ddd2c5f6291a3bd3 (patch) | |
tree | dd23868b01e3c0b2969ea6fa17aed7b0e11afd6d /generic | |
parent | fd9b1212b63785d7938a48b81f8c7700166aedd1 (diff) |
Add fix and regression test for Trac #138
Diffstat (limited to 'generic')
-rw-r--r-- | generic/proof-shell.el | 52 |
1 files changed, 23 insertions, 29 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index f26dffc3..4015f3a8 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -920,34 +920,27 @@ If the proof shell is busy when this function is called, then QUEUEMODE must match the mode of the queue currently being processed." - (let ((nothingthere (null proof-action-list)) - (nothingnew (null queueitems))) + (when (and queueitems proof-action-list) + ;; internal check: correct queuemode in force if busy + ;; (should have proof-action-list<>nil -> busy) + (and proof-shell-busy queuemode + (unless (eq proof-shell-busy queuemode) + (proof-debug + "proof-append-alist: wrong queuemode detected for busy shell") + (assert (eq proof-shell-busy queuemode))))) + + + (let ((nothingthere (null proof-action-list))) + ;; Now extend or start the queue. + (setq proof-action-list + (nconc proof-action-list queueitems)) - (if (and nothingthere nothingnew) - ;; remove the queue (otherwise done in proof-shell-exec-loop) - (proof-detach-queue) - - (unless nothingnew - - (when (and queueitems proof-action-list) - ;; internal check: correct queuemode in force if busy - ;; (should have proof-action-list<>nil -> busy) - (and proof-shell-busy queuemode - (unless (eq proof-shell-busy queuemode) - (proof-debug - "proof-append-alist: wrong queuemode detected for busy shell") - (assert (eq proof-shell-busy queuemode))))) - - ;; Now extend or start the queue. - (setq proof-action-list - (nconc proof-action-list queueitems)) - - (when nothingthere ; process comments immediately - (let ((cbitems (proof-shell-slurp-comments))) - (mapc 'proof-shell-invoke-callback cbitems))) - - (when proof-action-list ; still something to do - + (when nothingthere ; process comments immediately + (let ((cbitems (proof-shell-slurp-comments))) + (mapc 'proof-shell-invoke-callback cbitems))) + + (if proof-action-list ;; something to do + (progn (if (proof-shell-should-be-silent) ;; do this ASAP, either first or just after current command (setq proof-action-list @@ -957,11 +950,12 @@ being processed." (cons (car proof-action-list) ; after current (cons (proof-shell-start-silent-item) (cdr proof-action-list)))))) - (when nothingthere ; start sending commands (proof-grab-lock queuemode) (setq proof-shell-last-output-kind nil) - (proof-shell-insert-action-item (car proof-action-list)))))))) + (proof-shell-insert-action-item (car proof-action-list)))) + ;; nothing to do: maybe we completed a list of comments without sending them + (proof-detach-queue)))) ;;;###autoload |