diff options
| -rw-r--r-- | coq/coq-abbrev.el | 2 | ||||
| -rw-r--r-- | coq/coq.el | 7 |
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] @@ -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") |