diff options
| author |  Hendrik Tews <hendrik@askra.de> | 2012-08-14 09:50:13 +0000 |
|---|---|---|
| committer | Hendrik Tews <hendrik@askra.de> | 2012-08-14 09:50:13 +0000 |
| commit | a5255e9d42efa6586f91ae638cad3956efc0e93c (patch) | |
| tree | 524391feb3a1b693d5723d6a230dfdc600460670 /generic | |
| parent | 35e28eca4daf3d39212e491a60eefb2efbec0fcb (diff) | |
fix 443 by enforcing that the prover is not busy in proof-retract-until-point
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 4ddb0045..d1c469a4 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2219,8 +2219,11 @@ user hasn't saved the latest edits. Therefore it is right to query saves here." (if (proof-locked-region-empty-p) (error "No locked region") - ;; enforces not busy (future: may allow retracting from queue in progress) (proof-activate-scripting) + ;; enforce not busy to avoid retracting items from the queue region, + ;; which is not supported currently, see #443 + ;; (future: may allow retracting from queue in progress) + (proof-shell-ready-prover) (unless (proof-locked-region-empty-p) ;; re-opening may discard locked region! (let ((span (span-at (point) 'type))) ;; If no span at point, retracts the last span in the buffer. |