Fixed experimental feature of storing response or goal in a persistent

buffer.

2 files changed, 8 insertions, 1 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index 77fe7384..5d179cd3 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -82,6 +82,8 @@
     ["Print..." coq-Print t]
     ["Check..." coq-Check t]
     ["About..." coq-About t]
+    [ "Store response" proof-store-response-win t]
+    [ "Store goal" proof-store-goals-win t]
     ("OTHER QUERIES"
      ["Print Hint" coq-PrintHint t]
      ["Show ith goal..." coq-Show t]
diff --git a/coq/coq.el b/coq/coq.el
index 034eb910..9291ab01 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -298,6 +298,7 @@ Initially 1 because Coq initial state has number 1.")
       (goto-char (point-min)))
     (if erase (copy-to-buffer nb (point-min) (point-max))
       (append-to-buffer nb (point-min) (point-max)))
+;    (set-window-point window pos)
     nb))
 
 ;; copy the content of proof-response-buffer into the "response-freeze" buffer,
@@ -308,7 +309,11 @@ Initially 1 because Coq initial state has number 1.")
     (let ((newbuffer nil))
       (set-buffer buffer)
       (setq newbuffer (proof-clone-buffer "*response-freeze*" erase))
-      (display-buffer-other-frame newbuffer))))
+      (let ((win (display-buffer-other-frame newbuffer))
+            (win-point-min (save-window-excursion
+                             (switch-to-buffer-other-frame newbuffer)
+                             (point-min))))
+      (set-window-point win win-point-min)))))
 
 (defun proof-store-response-win (&optional erase)
   (interactive "P")