diff options
Diffstat (limited to 'generic/proof-script.el')
| -rw-r--r-- | generic/proof-script.el | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fb8d1199..014b99ff 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -1973,6 +1973,19 @@ the proof script." (proof-retract-until-point-interactive)) (proof-maybe-follow-locked-end)) +(defun proof-retract-current-goal () + "Retract the current proof, and move point to its start." + (interactive) + (proof-maybe-save-point + (let + ((span (proof-last-goal-or-goalsave))) + (if (and span (not (eq (span-property span 'type) 'goalsave)) + (< (span-end span) (proof-unprocessed-begin))) + (progn + (goto-char (span-start span)) + (proof-retract-until-point-interactive) + (proof-maybe-follow-locked-end)) + (error "Not proving"))))) ;; ;; Interrupt |