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.

2 files changed, 38 insertions, 34 deletions

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