Made new command proof-cd to cd to the directory of the current

buffer.  Added a version of it to proof-activate-scripting-hook.
Removed cd from initialization sequence.
Changed prover specifics accordingly.

5 files changed, 43 insertions, 39 deletions

diff --git a/coq/coq.el b/coq/coq.el
index a2df7a0c..4b0f6070 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -65,8 +65,7 @@
 
 ;; Command to initialize the Coq Proof Assistant
 (defconst coq-shell-init-cmd 
-  (concat (format "Set Undo %s.\n" coq-default-undo-limit)
-	  (format "Cd \"%s\"." default-directory)))
+  (format "Set Undo %s" coq-default-undo-limit))
 
 ;; Command to reset the Coq Proof Assistant
 (defconst coq-shell-restart-cmd 
@@ -75,7 +74,8 @@
 (defvar coq-shell-prompt-pattern (concat "^" proof-id " < ")
   "*The prompt pattern for the inferior shell running coq.")
 
-(defvar coq-shell-cd nil ; "Cd \"%s\"."
+;; FIXME da: this was disabled (set to nil) -- why?
+(defvar coq-shell-cd "Cd \"%s\""
   "*Command of the inferior process to change the directory.") 
 
 (defvar coq-shell-abort-goal-regexp "Current goal aborted"
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 40d66df1..175906d7 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1618,15 +1618,18 @@ returns false, then an error message is given."
      (error "Proof General not configured for this: set %s" 
 	    ,(symbol-name var))))
 
-(defmacro proof-define-assistant-command (fn doc cmdvar)
-  "Define command FN to send string CMDVAR to proof assistant."
+(defmacro proof-define-assistant-command (fn doc cmdvar &optional body)
+  "Define command FN to send string BODY to proof assistant, based on CMDVAR.
+BODY defaults to CMDVAR, a variable."
   `(defun ,fn ()
-     ,(concat doc "\nIssues a command to the assistant from " 
-	      (symbol-name cmdvar) ".")
+     ,(concat doc 
+	      (concat "\nIssues a command to the assistant based on " 
+		      (symbol-name cmdvar) ".") 
+		"")
      (interactive)
      (proof-if-setting-configured ,cmdvar
        (proof-shell-invisible-command
-	(concat ,cmdvar proof-terminal-string)))))
+	(concat ,(or body cmdvar) proof-terminal-string)))))
 
 (defmacro proof-define-assistant-command-witharg (fn doc cmdvar prompt &rest body)
   "Define command FN to prompt for string CMDVAR to proof assistant.
@@ -1681,6 +1684,21 @@ Start up the proof assistant if necessary."
   "Show a help or information message from the proof assistant.
 Typically, a list of syntax of commands available."
   proof-info-command)
+(proof-define-assistant-command proof-cd
+  "Change directory to the default directory for the current buffer."
+  proof-shell-cd
+  (format proof-shell-cd
+	  ;; Use expand-file-name to avoid problems with dumb
+	  ;; proof assistants and "~"
+	  (expand-file-name (default-directory))))
+
+(defun proof-cd-sync ()
+  "If proof-shell-cd is set, do proof-cd and wait for prover ready.
+This is intended as a value for proof-activate-scripting-hook"
+  (if proof-shell-cd 
+      (progn
+	(proof-cd)
+	(proof-shell-wait))))
 
 ;;
 ;; Commands which require an argument, and maybe affect the script.
@@ -1903,8 +1921,15 @@ sent to the assistant."
 \\{proof-mode-map}"
   (setq proof-buffer-type 'script)
 
+  ;; We set hook functions here rather than in proof-config-done
+  ;; so that they can be adjusted by prover specific code
+  ;; if need be.
+
   (make-local-hook 'kill-buffer-hook)
-  (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)))
+  (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
+
+  (make-local-hook 'proof-activate-script-hook) ; necessary?
+  (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t)))
 
 (defun proof-script-kill-buffer-fn ()
   "Value of kill-buffer-hook for proof script buffers.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index dd04b3ee..5a850556 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1507,7 +1507,8 @@ Calls proof-state-change-hook."
 
 (defun proof-shell-invisible-command (cmd &optional wait)
   "Send CMD to the proof process.
-If optional WAIT command is non-nil, wait for processing to finish
+By default, let the command be processed asynchronously.
+But if optional WAIT command is non-nil, wait for processing to finish
 before and after sending the command."
   (if wait (proof-shell-wait))
   (proof-shell-ready-prover)
@@ -1626,38 +1627,16 @@ before and after sending the command."
       (add-hook 'kill-buffer-hook 'proof-shell-kill-function t t)
       (set-process-sentinel proc 'proof-shell-bail-out)
 
-      ;; Flush pending output from startup
-      (accept-process-output proc 1)
-
-      ;; If the proof process in invoked on a different machine e.g.,
-      ;; for proof-prog-name="ssh fastmachine proofprocess", one needs
-      ;; to adjust the directory. Perhaps one might even want to issue
-      ;; this command whenever a new scripting buffer is active?
-
-      ;; This is the last unsynchronized input to the process.
-      ;; It would be better to synchronize it but then we lose
-      ;; any startup messages from proof-shell-init-cmd.
-
-      (if (and proof-shell-cd t) ;  proof-rsh-command)
- 	  (proof-shell-insert
-	   (format proof-shell-cd
-		   ;; under Emacs 19.34 default-directory contains "~"
-		   ;; which causes problems with LEGO's internal Cd
-		   ;; command
-		   (expand-file-name default-directory))))
-
-      ;; Try to flush the output from the cd command.
+      ;; Flush pending output from startup 
+      ;; (it gets hidden from the user)
       (accept-process-output proc 1)
 
       ;; Send intitialization command and wait for it to be
-      ;; processed.   This also ensures proof-action-list is
+      ;; processed.   Also ensure that proof-action-list is
       ;; initialised. 
       (if proof-shell-init-cmd
-	  (proof-shell-invisible-command proof-shell-init-cmd t)))))
-
-      ;; Set proof marker to current end of buffer
-      ;; (temp hack for old code)
-      ;;(set-marker proof-marker (point-max))))))
+	  (proof-shell-invisible-command proof-shell-init-cmd t)
+	(setq proof-action-list nil)))))
 
 (eval-and-compile
 (define-derived-mode proof-universal-keys-only-mode fundamental-mode
diff --git a/isa/isa.el b/isa/isa.el
index 7440ac06..9482e3dc 100644
--- a/isa/isa.el
+++ b/isa/isa.el
@@ -161,7 +161,7 @@ no regular or easily discernable structure."
    proof-shell-prompt-pattern		"^2?[-=#>]>? *"
 
    ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd			"cd \"%s\";"
+   proof-shell-cd			"cd \"%s\""
 
    ;; FIXME: the next two are probably only good for NJ/SML
    proof-shell-error-regexp		"^.*Error:\\|^\364\\*\\*\\*"
diff --git a/isar/isar.el b/isar/isar.el
index 9b00c6ca..c608c980 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -190,7 +190,7 @@
    proof-shell-prompt-pattern		"^\\w*[>#] "
 
    ;; for issuing command, not used to track cwd in any way.
-   proof-shell-cd			(isar-verbatim "cd \"%s\";")
+   proof-shell-cd			(isar-verbatim "cd \"%s\"")
 
    proof-shell-proof-completed-regexp   nil     ; n.a.
    proof-shell-interrupt-regexp         "\364\\*\\*\\* Interrupt\\|\360Interrupt"