diff options
author | Pierre Courtieu <courtieu@lri.fr> | 2008-05-20 11:11:34 +0000 |
---|---|---|
committer | Pierre Courtieu <courtieu@lri.fr> | 2008-05-20 11:11:34 +0000 |
commit | 91b0057e6994708f39b8ebde6dd14cb55de52f5d (patch) | |
tree | 3810adce60335433d35f991d15f903d48958414a | |
parent | 82ab48dd8ffc7ae698512f63cb8bb2ba97c16fe4 (diff) |
Fixed a bug with coq-prog-name.
-rw-r--r-- | coq/coq-local-vars.el | 68 | ||||
-rw-r--r-- | coq/coq-syntax.el | 6 | ||||
-rw-r--r-- | coq/coq.el | 48 | ||||
-rw-r--r-- | lib/local-vars-list.el | 13 |
4 files changed, 80 insertions, 55 deletions
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index 396d6f6e..effa3d02 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -78,20 +78,31 @@ Set them to PROGNAME and PROGARGS respectively. These variables describe the coqtop command to be launched on this file." (local-vars-list-set 'coq-prog-name progname) (local-vars-list-set 'coq-prog-args progargs) - ) + (setq proof-prog-name progname) + (setq proof-prog-args progargs)) + (defun coq-read-directory (prompt &optional default maynotmatch initialcontent) - "Ask for (using PROMPT) and return a directory name. + "Ask for (using PROMPT) and return a directory name. Do not insert the default directory." (let* - ;; read-file-name here because it is convenient to see .v files - ;; when selecting directories to add to the path. Moreover - ;; read-directory-name does not seem to exist in fsf emacs?? - ((path (read-file-name prompt "" default (not maynotmatch) initialcontent))) + ;; read-file-name here because it is convenient to see .v files when + ;; selecting directories to add to the path. Moreover read-directory-name + ;; does not seem to exist in fsf emacs?? temporarily disable graphical + ;; dialog, as read-file-name does not allow to select a directory + ((current-use-dialog-box use-dialog-box) + (dummy (setq use-dialog-box nil)) + (fname (file-name-nondirectory default)) + (dir (file-name-directory default)) + (path + (read-file-name prompt dir fname (not maynotmatch) initialcontent))) + (setq use-dialog-box current-use-dialog-box) path)) +;(read-file-name prompt &optional dir default-filename mustmatch +; initial predicate) ;(read-from-minibuffer -; PROMPT &optional INITIAL-CONTENTS KEYMAP READP HISTORY ABBREV-TABLE DEFAULT) +; PROMPT &optional INITIAL-CONTENTS KEYMAP READP HISTORY ABBREV-TABLE DEFAULT) ;(read-directory-name ; PROMPT &optional DIR DEFAULT MUST-MATCH INITIAL-CONTENTS HISTORY) @@ -101,12 +112,12 @@ Do not insert the default directory." (let ((hd (car args)) (tl (cdr args))) (cond ((string-equal hd "-I") - (cond - ((not tl) nil) - ; if the option following -I starts with '-', forget the -I : - ((char-equal ?- (string-to-char (car tl))) - (coq-extract-directories-from-args tl)) - (t (cons (car tl) (coq-extract-directories-from-args (cdr tl)))))) + (cond + ((not tl) nil) + ; if the option following -I starts with '-', forget the -I : + ((char-equal ?- (string-to-char (car tl))) + (coq-extract-directories-from-args tl)) + (t (cons (car tl) (coq-extract-directories-from-args (cdr tl)))))) (t (coq-extract-directories-from-args tl)))))) @@ -116,18 +127,20 @@ These variable describes the coqtop arguments to be launched on this file. Optional argument OLDVALUE specifies the previous value of `coq-prog-args', it will be used to suggest values to the user." (let* ((olddirs (coq-extract-directories-from-args oldvalue)) - (progargs (if coq-version-is-V8-1 '("-emacs-U") '("-emacs"))) - (option)) - ;; first suggest preious directories + (progargs (if coq-version-is-V8-1 '("-emacs-U") '("-emacs"))) + (option)) + ;; first suggest previous directories (while olddirs (if (y-or-n-p (format "Keep the directory %s? " (car olddirs))) - (setq progargs (cons (car olddirs) (cons "-I" progargs)))) + (setq progargs (cons (car olddirs) (cons "-I" progargs)))) (setq olddirs (cdr olddirs))) ;; then ask for more - (setq option (coq-read-directory "Add directory (tab to complete, empty to stop) :" "")) + (setq option (coq-read-directory + "Add directory (tab to complete, empty to stop) -I:" "")) (while (not (string-equal option "")) (setq progargs (cons option (cons "-I" progargs))) ;reversed - (setq option (coq-read-directory "Add directory (tab to complete, empty to stop) -I :" ""))) + (setq option (coq-read-directory + "Add directory (tab to complete, empty to stop) -I :" ""))) (reverse progargs))) (defun coq-ask-prog-name (&optional oldvalue) @@ -135,13 +148,16 @@ will be used to suggest values to the user." These variable describes the coqtop command to be launched on this file. Optional argument OLDVALUE specifies the previous value of `coq-prog-name', it will be used to suggest a value to the user." + (message (concat "oldavalue: " oldvalue)) (let* ((deflt (or oldvalue "coqtop")) - (cmd (coq-read-directory "coq program name (default \"coqtop\"): " - deflt t deflt))) + (cmd (coq-read-directory + (concat "coq program name (default \"" oldvalue "\"): ") + deflt t)) + (cmd (if (string-equal cmd "") oldvalue cmd))) (if (and (string-match " " cmd) (not (y-or-n-p "The prog name contains spaces, are you sure ? "))) - (coq-ask-prog-name) ; retry + (coq-ask-prog-name oldvalue) ; retry cmd))) @@ -150,12 +166,10 @@ will be used to suggest a value to the user." These variables describe the coqtop command to be launched on this file." (interactive) (let* ((oldname (local-vars-list-get-safe 'coq-prog-name)) - (oldargs (local-vars-list-get-safe 'coq-prog-args)) - (progname (coq-ask-prog-name oldname)) + (oldargs (local-vars-list-get-safe 'coq-prog-args)) + (progname (coq-ask-prog-name oldname)) (progargs (coq-ask-prog-args oldargs))) - (coq-insert-coq-prog-name progname progargs) - (setq coq-prog-name progname) - (setq coq-prog-args progargs))) + (coq-insert-coq-prog-name progname progargs))) diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index c7a96fef..af6aa6b1 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -12,10 +12,10 @@ (defcustom coq-prog-name ;; da: moved from coq.el since needed here (proof-locate-executable "coqtop" t '("C:/Program Files/Coq/bin")) - "*Name of program to run as Coq. See `proof-prog-name', which is set from this. - On Windows with latest Coq package you might need something like: + "*Name of program to run as Coq. See `proof-prog-name', which is set from + this. On Windows with latest Coq package you might need something like: C:/Program Files/Coq/bin/coqtop.opt.exe - instead of just \"coqtop\". + instead of just \"coqtop\". This must be a single program name with no arguments; see `coq-prog-args' to manually adjust the arguments to the Coq process. See also `coq-prog-env' to adjust the environment." @@ -787,20 +787,29 @@ This is specific to `coq-mode'." (defun coq-guess-command-line (filename) "Guess the right command line options to compile FILENAME using `make -n'." - (let ((dir (file-name-directory filename))) - (if (file-exists-p (concat dir "Makefile")) - (let* - ((compiled-file (concat (substring - filename 0 - (string-match ".v$" filename)) ".vo")) - (command (shell-command-to-string - (concat "cd " dir ";" - "gmake -n -W " filename " " compiled-file - "| sed s/coqc/coqtop/")))) - (concat - (substring command 0 (string-match " [^ ]*$" command)) - (if coq-version-is-V8-1 '("-emacs-U") '("-emacs")))) - coq-prog-name))) + (if (local-variable-p 'coq-prog-name (current-buffer)) coq-prog-name + (let ((dir (file-name-directory filename)) + (makedir + (cond + ((file-exists-p (concat dir "Makefile")) ".") +; ((file-exists-p (concat dir "../Makefile")) "..") +; ((file-exists-p (concat dir "../../Makefile")) "../..") + (t nil)))) + (if makedir + (let* + ;;TODO, add dir name when makefile is in .. or ../.. + ((compiled-file (concat (substring + filename 0 + (string-match ".v$" filename)) ".vo")) + (command (shell-command-to-string + (concat "cd " dir ";" + "gmake -n -W " filename " " compiled-file + "| sed s/coqc/coqtop/")))) + (concat + (substring command 0 (string-match " [^ ]*$" command)) + (if coq-version-is-V8-1 '("-emacs-U") '("-emacs")))) + coq-prog-name)))) + ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Configuring proof and pbp mode and setting up various utilities ;; @@ -818,15 +827,16 @@ This is specific to `coq-mode'." (setq proof-assistant-home-page coq-www-home-page) - (setq proof-prog-name coq-prog-name) + (setq proof-prog-name coq-prog-name) (setq proof-guess-command-line 'coq-guess-command-line) + (setq proof-prog-name-guess t) ;; Commands sent to proof engine (setq proof-showproof-command "Show. " - proof-context-command "Print All. " - proof-goal-command "Goal %s . " - proof-save-command "Save %s . " - proof-find-theorems-command "Search %s . ") + proof-context-command "Print All. " + proof-goal-command "Goal %s . " + proof-save-command "Save %s . " + proof-find-theorems-command "Search %s . ") ;; FIXME da: Does Coq have a help or about command? ;; proof-info-command "Help" diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index e6221e9a..f0b6678e 100644 --- a/lib/local-vars-list.el +++ b/lib/local-vars-list.el @@ -186,18 +186,19 @@ Raises an error if symb is not in the list." (local-vars-list-get-current lpat rpat)))) (defun local-vars-list-get-safe (symb) - "Return true if variable SYMB belongs to the local variable list of the current -buffer." + "Return true if variable SYMB belongs to the local variable list of the +current buffer." (condition-case nil (local-vars-list-get symb) (error nil))) (defun local-vars-list-set (symb val) "Write the value val in the local variable list for variable symb. -If the variable is already specified in the list, replace the value. If no local -variable list is found, create one at the end of the buffer first." +If the variable is already specified in the list, replace the +value. If no local variable list is found, create one at the end +of the buffer first." (save-excursion (let ((lrpat (local-vars-list-find))) - (if (not lrpat) - (progn + (if (not lrpat) + (progn (local-vars-list-insert-empty-zone) (setq lrpat (local-vars-list-find)))) (beginning-of-line) |