diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 11:11:18 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-08-25 11:11:18 +0000 |
| commit | 8f23b61efea192d249f82c57f15f7fe966850f9a (patch) | |
| tree | 5d0ae5da809c7482852a96a6cda397808aa00674 /generic | |
| parent | 6da866a789b7cd5b113d465c08714bce9d560065 (diff) | |
proof-retract-before-change: now interrupts are robust in Isabelle, try
interrupting if prover is busy before undoing. Refs Trac #293
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 069b7046..48d961d1 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1917,14 +1917,16 @@ that these may be overwritten)." (defun proof-retract-before-change (beg end) "For `before-change-functions'. Retract to BEG unless BEG and END in comment. No effect if prover is busy." - (and (> (proof-queue-or-locked-end) beg) - (not (and (proof-inside-comment beg) - (proof-inside-comment end))) - (if proof-shell-busy - (error "Prover busy") - (save-excursion - (goto-char beg) - (proof-retract-until-point))))) + (when (and (> (proof-queue-or-locked-end) beg) + (not (and (proof-inside-comment beg) + (proof-inside-comment end)))) + (when proof-shell-busy + (message "Interrupting prover") + (proof-interrupt-process) + (proof-shell-wait)) + (save-excursion + (goto-char beg) + (proof-retract-until-point)))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |