diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index 3a24595e..e67a7774 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1240,12 +1240,16 @@ activation is considered to have failed and an error is given." (assert (null proof-script-buffer) "Bug in proof-activate-scripting: deactivate failed.") - ;; Set the active scripting buffer, and initialise regions + ;; Set the active scripting buffer (setq proof-script-buffer (current-buffer)) ;; Fire up the prover (or check it's going the right way). - (proof-shell-ready-prover queuemode) + (condition-case-unless-debug err + (proof-shell-ready-prover queuemode) + (error (setq proof-script-buffer nil) + (signal (car err) (cdr err)))) + ;; Initialise regions (if (proof-locked-region-empty-p) ; leave alone if non-empty (proof-init-segmentation)) @@ -1985,11 +1989,12 @@ No effect if prover is busy." (proof-interrupt-process) (proof-shell-wait)) (save-excursion - (save-restriction ;; see Trac#403 - (widen) - (goto-char beg) - (proof-retract-until-point) - (proof-shell-wait))))) + (save-match-data ;; see PG#41 + (save-restriction ;; see Trac#403 + (widen) + (goto-char beg) + (proof-retract-until-point) + (proof-shell-wait)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |