From 0d652f0ee9e925ac7fa3539cb4b18973a4ce04dd Mon Sep 17 00:00:00 2001
From: Thomas Kleymann
Date: Wed, 13 Nov 1996 14:57:54 +0000
Subject: 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
---
 ext.el | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

(limited to 'ext.el')

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