aboutsummaryrefslogtreecommitdiffhomepage
path: root/generic
diff options
context:
space:
mode:
authorGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-06-10 17:15:29 -0400
committerGravatar Clément Pit--Claudel <clement.pitclaudel@live.com>2016-06-10 17:37:01 -0400
commit493211dbd924520e6842f3e5d7c8fd1b3cbf1485 (patch)
treec2128f9a2cf99714038a17522bc9ae4aa13a057b /generic
parentb4ed3cf3ce09c397115e7f75372245724410a187 (diff)
Reset proof-script-buffer to nil if -ready-prover fails
Fixes #65
Diffstat (limited to 'generic')
-rw-r--r--generic/proof-script.el8
-rw-r--r--generic/proof-shell.el5
2 files changed, 10 insertions, 3 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 3a24595e..a9c55353 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))
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 4f89963e..64eee4c8 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -379,7 +379,10 @@ process command."
(setq proof-shell-buffer (get-buffer (concat "*" proc "*")))
(unless (proof-shell-live-buffer)
- ;; Give error now if shell buffer isn't live (process exited)
+ ;; Give error now if shell buffer isn't live (process exited). We also
+ ;; set the process filter to nil to avoid processing error messages
+ ;; related to the process exit.
+ (set-process-filter (get-buffer-process proof-shell-buffer) nil)
(setq proof-shell-buffer nil)
(error "Starting process: %s..failed" prog-command-line)))