diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 20:13:04 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2008-01-31 20:13:04 +0000 |
commit | cd72e777964d01cd3ebe36da121b19176d0b80d1 (patch) | |
tree | 25a7265d16988c8f582e3820b483856799d07ffe /generic | |
parent | f7ac8fc315a22e5fa949ca33f0fe1e66d156eca1 (diff) |
Sendback commands from response buffer sent via assert-until-point, with ordinary span construction.
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))) |