diff options
| -rw-r--r-- | generic/proof-shell.el | 52 | ||||
| -rw-r--r-- | isar/isar-autotest.el | 10 |
2 files changed, 33 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 diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index f24e3450..a98dc664 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -46,6 +46,7 @@ (proof-shell-wait) (pg-autotest eval (proof-process-buffer)) (pg-autotest assert-full) + ;; Speed up prover (pg-autotest eval (isar-tracing:auto-quickcheck-toggle 0)) @@ -69,6 +70,15 @@ (pg-autotest eval (insert "end")) (proof-electric-terminator) (pg-autotest assert-full) + ;; Test Trac#138 + (pg-autotest eval (proof-undo-last-successful-command)) + (proof-shell-wait) + (pg-autotest eval (proof-goto-end-of-locked)) + (pg-autotest eval (insert "(* this is a comment *)")) + (pg-autotest eval (proof-goto-point)) + (proof-shell-wait) + (pg-autotest eval (skip-chars-backward " \n\t")) + (pg-autotest eval (insert " ")) ;; shouldn't give read-only error! (set-buffer-modified-p nil) (kill-buffer ".autotest.thy") |