Added completion to coq-prog-name asking.

2 files changed, 6 insertions, 4 deletions

diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 55adc061..581a6a80 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -81,13 +81,13 @@ coqtop command to be launched on this file."
   )
 
 
-(defun coq-read-directory (prompt)
+(defun coq-read-directory (prompt &optional maynotmatch initialcontent)
   "Ask for (using PROMPT) and return a directory name."
   (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 "" "" t)))
+      ((path (read-file-name prompt "" "" (not maynotmatch) initialcontent)))
     path))
 
 ;(read-from-minibuffer
@@ -135,7 +135,7 @@ 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."
-  (let ((cmd (read-string "coq program name (default coqtop) : "
+  (let ((cmd (coq-read-directory "coq program name (default coqtop) : " t
 			  (or oldvalue "coqtop"))))
     (if (and
          (string-match " " cmd)
diff --git a/coq/coq.el b/coq/coq.el
index d5e120e3..c3edeb7f 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -66,7 +66,9 @@ To disable coqc being called (and use only make), set this to nil."
 (require 'coq-syntax)
 (require 'coq-indent)
 
-(defcustom coq-utf-safe "" nil)
+(defcustom coq-utf-safe nil 
+  "Should be t if one wants no multibyte characters be used for 
+controling coq prompt. Only for coq >= 8.1 (and 8.1 beta)")
 (if (and coq-utf-safe coq-version-is-V8-1) (setq coq-prog-args '("-emacs-U"))
   (setq coq-prog-args '("-emacs")))