diff options
| -rw-r--r-- | coq/coq.el | 18 | ||||
| -rw-r--r-- | coq/ex/test-cases/README | 1 | ||||
| -rw-r--r-- | coq/ex/test-cases/stale-load-path/README | 4 | ||||
| -rw-r--r-- | coq/ex/test-cases/stale-load-path/a/.cvsignore | 2 | ||||
| -rw-r--r-- | generic/proof-shell.el | 10 |
5 files changed, 29 insertions, 6 deletions
@@ -1095,14 +1095,12 @@ Currently this doesn't take the loadpath into account." ;; ;; TODO list: -;; - restart coqtop on buffer switch ;; - update patch website ;; - display coqdep errors in the recompile-response buffer ;; - use a variable for the recompile-response buffer ;; - fix problem with partial library names ;; - clean old multiple file stuff ;; - fix places marked with XXX -;; - test and fix problems when switchen scripting between different directories ;; - enable next-error in recompile-response buffers ;; - call compile more cleverly, with a coq-specific option for compile ;; command confirmation @@ -1642,6 +1640,22 @@ compilation (if necessary) of the dependencies." (add-hook 'proof-shell-extend-queue-hook 'coq-preprocess-require-commands) +;; kill coqtop on script buffer change + +(defun coq-switch-buffer-kill-proof-shell () + "Kill the proof shell without asking the user. +This function is for `proof-deactivate-scripting-hook'. It kills +the proof shell without asking the user for +confirmation (assuming she agreed already on switching the active +scripting buffer). This is needed to ensure the load path is +correct in the new scripting buffer." + (proof-shell-exit t)) + + +(add-hook 'proof-deactivate-scripting-hook + 'coq-switch-buffer-kill-proof-shell + t) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; ;; Pre-processing of input string diff --git a/coq/ex/test-cases/README b/coq/ex/test-cases/README index 7d91b29f..b89cc230 100644 --- a/coq/ex/test-cases/README +++ b/coq/ex/test-cases/README @@ -26,4 +26,3 @@ retract-completely-asserted stale-load-path test switching between files with different load path. - (triggers known bugs) diff --git a/coq/ex/test-cases/stale-load-path/README b/coq/ex/test-cases/stale-load-path/README index 343fe85a..273368cd 100644 --- a/coq/ex/test-cases/stale-load-path/README +++ b/coq/ex/test-cases/stale-load-path/README @@ -8,6 +8,10 @@ Project b depends on a, more precisely, b/b.v requires a/Le.v. File c/c.v require Le, but this refers to Coq.Arith.Le!! +The resulting LoadPath confusion bug, which is described in the +following, has been fixed with the commit +around 2011-01-18 21:45:00 UTC. + Currently coqtop is not able to reset the LoadPath, therefore, when first scripting b/b.v and then switching to c/c.v, coq wrongly loads a/Le.vo! Vice versa, when first scripting c/c.v and diff --git a/coq/ex/test-cases/stale-load-path/a/.cvsignore b/coq/ex/test-cases/stale-load-path/a/.cvsignore new file mode 100644 index 00000000..e940bcb4 --- /dev/null +++ b/coq/ex/test-cases/stale-load-path/a/.cvsignore @@ -0,0 +1,2 @@ +*.glob +*.vo diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 069694e7..fe439115 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -459,14 +459,18 @@ shell buffer, alled by `proof-shell-bail-out' if process exits." proof-shell-delayed-output-end nil proof-shell-delayed-output-flags nil)) -(defun proof-shell-exit () +(defun proof-shell-exit (&optional dont-ask) "Query the user and exit the proof process. This simply kills the `proof-shell-buffer' relying on the hook function -`proof-shell-kill-function' to do the hard work." + +`proof-shell-kill-function' to do the hard work. If optional +argument DONT-ASK is non-nil, the proof process is terminated +without confirmation." (interactive) (if (buffer-live-p proof-shell-buffer) - (when (yes-or-no-p (format "Exit %s process? " proof-assistant)) + (when (or dont-ask + (yes-or-no-p (format "Exit %s process? " proof-assistant))) (let ((kill-buffer-query-functions nil)) ; avoid extra dialog (kill-buffer proof-shell-buffer)) (setq proof-shell-buffer nil)) |