diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 10:12:10 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2007-08-19 10:12:10 +0000 |
| commit | c77ef0877c803f1a2e38bed773a961b107cb469b (patch) | |
| tree | 15e3fa3d77d11a180b185e1e277698687bbbba7e | |
| parent | be86be871f67097155104ce3dfdf2e982d39b543 (diff) | |
proof-append-alist: detach queue span if no commands after comments stripped.
Fixes trac report #138: processing comments alone leads to spurious read-only region.
| -rw-r--r-- | generic/proof-shell.el | 16 |
1 files changed, 5 insertions, 11 deletions
diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 7b2b034c..e97fdd52 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1096,13 +1096,16 @@ If the proof shell is busy when this function is called, then QUEUEMODE must match the mode of the queue currently being processed." (let (item) - ;; FIXME: may be wrong time to invoke callbacks for no-op commands, - ;; if the queue is not empty. + ;; NB: wrong time for callbacks for no-op commands, if queue non-empty. (while (and alist (string= (nth 1 (setq item (car alist))) proof-no-command)) (funcall (nth 2 item) (car item)) (setq alist (cdr alist))) + (if (and (null alist) (null proof-action-list)) + ;; remove the queue (otherwise done in proof-shell-exec-loop) + (proof-detach-queue)) + (if alist (if proof-action-list (progn @@ -1234,9 +1237,6 @@ and indentation. Assumes proof-script-buffer is active." (with-current-buffer proof-script-buffer (let (span) (proof-goto-end-of-locked) - ;; Fix 16.11.99. This attempts to indent current line which can - ;; be read-only. - ;; (newline-and-indent) (let ((proof-one-command-per-line t)) ; because pbp several commands (proof-script-new-command-advance)) (insert cmd) @@ -1257,12 +1257,6 @@ and indentation. Assumes proof-script-buffer is active." (cons (list span cmd 'proof-done-advancing) (cdr proof-action-list)))))))) -;; da: first note of this sentence is false! -;; ******** NB ********** -;; While we're using pty communication, this code is OK, since all -;; eager annotations are one line long, and we get input a line at a -;; time. If we go over to piped communication, it will break. - (defun proof-shell-message (str) "Output STR in minibuffer." ;; %s is used below to escape characters special to |