aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDavid Aspinall2009-09-10 22:31:13 +0000
committerDavid Aspinall2009-09-10 22:31:13 +0000
commitfd9544327956e2ac0ae6eff9845bc379f941de6f (patch)
tree8410f7cb539c858d8357efd6345ebaaa6d86f5f4
parent2242c8ec1ea3886d4b1d73ef534ba9763031f6ad (diff)
proof-retract-until-point: protect against finding no span at all
(mask current bug in Coq code)
-rw-r--r--generic/proof-script.el6
1 files changed, 5 insertions, 1 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el
index c6050abd..38feb34a 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -2222,7 +2222,11 @@ command."
(proof-goto-end-of-locked)
(backward-char)
(setq span (span-at (point) 'type)))
- (proof-retract-target span delete-region)))))
+ (if span
+ (proof-retract-target span delete-region)
+ ;; something wrong
+ (proof-debug
+ "proof-retract-until-point: couldn't find a span!"))))))