From cd72e777964d01cd3ebe36da121b19176d0b80d1 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Thu, 31 Jan 2008 20:13:04 +0000
Subject: Sendback commands from response buffer sent via assert-until-point,
 with ordinary span construction.

---
 generic/proof-script.el | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'generic')

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)))
 
 
 
-- 
cgit v1.2.3