Sendback commands from response buffer sent via assert-until-point, with ordinary span construction.

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)))