Yves Bertot:

  If you click on an hypothesis name or a goal name, then Emacs generates
  commands that are sent to lego but not stored in the script buffer.
  The fix I have is to replace pbp-construct-command

1 files changed, 9 insertions, 4 deletions

diff --git a/ext.el b/ext.el
index c35c4bec..ca2f9abc 100644
--- a/ext.el
+++ b/ext.el
@@ -164,6 +164,7 @@
    (mouse-set-point event)
    (pbp-construct-command))
 
+
 (defun pbp-construct-command ()
    (let ((ext (extent-at (point) () 'lego-pbp))
          (top-ext (extent-at (point) () 'lego-top-element)))
@@ -177,11 +178,15 @@
 		  (concat "Pbp " (cdr top-info) " " path ";")))))
 	    ((extentp top-ext)
 	     (let ((top-info (extent-property top-ext 'lego-top-element)))
-	       (proof-simple-send
-		(if (eq 'hyp (car top-info))
+	       (let ((value (if (eq 'hyp (car top-info))
 		    (concat "Refine " (cdr top-info) ";")
-		  (concat "Next +" (cdr top-info) ";"))))))))
-
+		  (concat "Next +" (cdr top-info) ";"))))
+	       (proof-simple-send
+		    value)
+		(if *script-buffer*
+		    (progn (set-buffer *script-buffer*)
+			   (end-of-buffer)
+			   (insert-string value)))))))))