- fixed stale load path problem with killing the proof shell in

  the deactivation-hook

4 files changed, 22 insertions, 3 deletions

diff --git a/coq/coq.el b/coq/coq.el
index 19e8dd62..ef3b3969 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -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