diff options
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/proof-script.el | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/generic/proof-script.el b/generic/proof-script.el index fafc25f4..8a01fd85 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -2225,6 +2225,14 @@ appropriate." (proof-start-queue (proof-unprocessed-begin) (point) (list (list span cmd 'proof-done-advancing))))) +;;;###autoload +(defun proof-insert-sendback-command (cmd) + "Insert CMD into the proof script, execute assert-until-point." + (let (span) + (proof-goto-end-of-locked) + (insert "\n") ;; could be user opt + (insert cmd) + (proof-assert-until-point))) |