Moved the coq local variables tools in a separate file and made it

simpler.

2 files changed, 138 insertions, 127 deletions

diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
new file mode 100644
index 00000000..f10ef6f1
--- /dev/null
+++ b/coq/coq-local-vars.el
@@ -0,0 +1,137 @@
+;;; coq-local-vars.el --- local variable list tools for coq
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Authors: Pierre Courtieu
+;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
+
+;; $Id$ 
+
+
+;;; Commentary:
+;; 
+
+
+;;; History:
+;; 
+
+(defconst coq-local-vars-doc nil
+  "A very convenient way to customize file-specific variables is to use the
+File Variables ((xemacs)File Variables). This feature of Emacs allows to
+specify the values to use for certain Emacs variables when a file is
+loaded. Those values are written as a list at the end of the file.
+
+We provide the following feature to help you:
+
+\\[coq-ask-insert-coq-prog-name] that builds standard local variable list for a
+coq file by asking you some questions. it is accessible in the menu:
+
+\"coq\"/\"set coq prog name for this file persistently\".
+
+You should be able to use this feature without reading the rest of this
+documentation, which explains how it is used for coq. For more precision, refer
+to the emacs info manual at ((xemacs)File Variables).
+
+In projects involving multiple directories, it is often useful to set the
+variables `proof-prog-name', `proof-prog-args' and `compile-command' for each
+file. Here is an example for Coq users: for the file .../dir/bar/foo.v, if you
+want Coq to be started with the path .../dir/theories/ added in the libraries
+path (\"-I\" option), you can put at the end of foo.v:
+
+(* 
+*** Local Variables: ***
+*** coq-prog-name: \"coqtop\" ***
+*** coq-prog-args: (\"-emacs\" \"-I\" \"../theories\") ***
+*** End: ***
+*)
+
+That way the good command is called when the scripting starts in foo.v. Notice
+that the command argument \"-I\" \"../theories\" is specific to the file foo.v,
+and thus if you set it via the configuration tool, you will need to do it each
+time you load this file. On the contrary with this method, Emacs will do this
+operation automatically when loading this file. Please notice that all the
+strings above should never contain spaces see documentation of variables
+`proof-prog-name' and `proof-prog-args'.
+
+Extending the previous example, if the makefile for foo.v is located in
+directory .../dir/, you can add the right compile command. And if you want a
+non standard coq executable to be used, here is what you should put in
+variables:
+
+(* 
+ Local Variables: 
+ coq-prog-name: \"../../coqsrc/bin/coqtop\" 
+ coq-prog-args: \"-emacs\" \"-I\" \"../theories\"
+ compile-command: \"make -C .. -k bar/foo.vo\" 
+ End:
+*)
+
+And then the right call to make will be done if you use the \\[compile]
+command. Notice that the lines are commented in order to be ignored by the
+proof assistant. It is possible to use this mechanism for any other buffer
+local variable (info:(xemacs)File Variables).
+" )
+
+
+(defun coq-insert-coq-prog-name (progname progargs)
+  "Insert or modify (if already existing) the local variables `coq-prog-name'
+and `coq-prog-args'.  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)
+  )
+
+
+(defun coq-ask-build-addpath-option ()
+  "Ask for 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
+      ((path (read-file-name "library path to add (empty to stop) : "
+                             "" "" t)))
+    (if (and (string-match " " path)
+             (not (y-or-n-p "The path contains spaces, are you sure? (y or n) :")))
+        (coq-ask-build-addpath-option) ; retry
+      path)))
+
+(defun coq-ask-prog-args ()
+  "Ask for and return the information to put into variables coq-prog-args.
+These variable describes the coqtop arguments to be launched on this file."  
+  (let ((progargs '("-emacs"))
+        (option (coq-ask-build-addpath-option)))
+    (message "progargs = %s" progargs)
+    (while (not (string-equal option ""))
+      (setq progargs (cons option (cons "-I" progargs))) ;reversed
+      (message "progargs = %s" progargs)
+      (setq option (coq-ask-build-addpath-option)))
+    (message "progargs = %s" progargs)
+    (reverse progargs)))
+
+(defun coq-ask-prog-name ()
+  "Ask for and return the local variables coq-prog-name.
+These variable describes the coqtop command to be launched on this file."  
+  (let ((cmd (read-string "coq program name (default coqtop) : " "coqtop")))
+    (if (and 
+         (string-match " " cmd)
+         (not (y-or-n-p "The prog name contains spaces, are you sure? (y or n) :")))
+        (coq-ask-prog-name) ; retry
+      cmd)))
+
+
+(defun coq-ask-insert-coq-prog-name ()
+  "Ask for and insert the local variables coq-prog-name and coq-prog-args.
+These variables describe the coqtop command to be launched on this file."  
+  (interactive)
+  (let ((progname (coq-ask-prog-name))
+        (progargs (coq-ask-prog-args)))
+    (coq-insert-coq-prog-name progname progargs)
+    (setq coq-prog-name progname)
+    (setq coq-prog-args progargs)))
+
+(provide 'coq-local-vars)
+
+
+;;   Local Variables: ***
+;;   fill-column: 79 ***
+;;   indent-tabs-mode: nil ***
+;;   End: ***
+
+;;; coq.el ends here
diff --git a/coq/coq.el b/coq/coq.el
index bb4c10fb..3d9ea9ed 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -16,6 +16,7 @@
 (require 'proof)
 (require 'holes-load) ; in lib directory
 (require 'local-vars-list) ; in lib directory
+(require 'coq-local-vars) ; in coq directory
 ;; coq-syntaxe is required below
 ;; ----- coq-shell configuration options
 
@@ -182,133 +183,6 @@ To disable coqc being called (and use only make), set this to nil."
 
 
 
-(defconst coq-local-vars-doc nil
-  "A very convenient way to customize file-specific variables is to use the
-File Variables ((xemacs)File Variables). This feature of Emacs allows to
-specify the values to use for certain Emacs variables when a file is
-loaded. Those values are written as a list at the end of the file.
-
-We provide the following feature to help you:
-
-\\[coq-ask-insert-coq-prog-name] that builds standard local variable list for a
-coq file by asking you some questions. it is accessible in the menu:
-
-\"coq\"/\"set coq prog name for this file persistently\".
-
-You should be able to use this feature without reading the rest of this
-documentation, which explains how it is used for coq. For more precision, refer
-to the emacs info manual at ((xemacs)File Variables).
-
-In projects involving multiple directories, it is often useful to set the
-variables `proof-prog-name', `proof-prog-args' and `compile-command' for each
-file. Here is an example for Coq users: for the file .../dir/bar/foo.v, if you
-want Coq to be started with the path .../dir/theories/ added in the libraries
-path (\"-I\" option), you can put at the end of foo.v:
-
-(* 
-*** Local Variables: ***
-*** coq-prog-name: \"coqtop\" ***
-*** coq-prog-args: (\"-emacs\" \"-I\" \"../theories\") ***
-*** End: ***
-*)
-
-That way the good command is called when the scripting starts in foo.v. Notice
-that the command argument \"-I\" \"../theories\" is specific to the file foo.v,
-and thus if you set it via the configuration tool, you will need to do it each
-time you load this file. On the contrary with this method, Emacs will do this
-operation automatically when loading this file. Please notice that all the
-strings above should never contain spaces see documentation of variables
-`proof-prog-name' and `proof-prog-args'.
-
-Extending the previous example, if the makefile for foo.v is located in
-directory .../dir/, you can add the right compile command. And if you want a
-non standard coq executable to be used, here is what you should put in
-variables:
-
-(* 
- Local Variables: 
- coq-prog-name: \"../../coqsrc/bin/coqtop\" 
- coq-prog-args: \"-emacs\" \"-I\" \"../theories\"
- compile-command: \"make -C .. -k bar/foo.vo\" 
- End:
-*)
-
-And then the right call to make will be done if you use the \\[compile]
-command. Notice that the lines are commented in order to be ignored by the
-proof assistant. It is possible to use this mechanism for any other buffer
-local variable (info:(xemacs)File Variables).
-" )
-
-
-
-(defun coq-insert-coq-prog-name (progname progargs)
-  "Insert the local variables coq-prog-name and coq-prog-args.
-These variables describe the coqtop command to be launched on this file."
-  (save-excursion
-    (goto-char (point-max))
-    (insert 
-     (format
-      "
-(* 
-   *** Local Variables: ***
-   *** coq-prog-name: %s ***
-   *** coq-prog-args: %s ***
-   *** End: ***
-*)"
-      progname progargs))))
-
-
-(defun coq-ask-build-addpath-option ()
-  "Ask for 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
-      ((path (read-file-name "library path to add (empty to stop) : "
-                             "" "" t)))
-    (if (and (string-match " " path)
-             (not (y-or-n-p "The path contains spaces, are you sure? (y or n) :")))
-        (coq-ask-build-addpath-option) ; retry
-      path)))
-
-(defun coq-ask-prog-args ()
-  "Ask for and return the information to put into variables coq-prog-args.
-These variable describes the coqtop arguments to be launched on this file."  
-  (let ((progargs '("-emacs"))
-        (option (coq-ask-build-addpath-option)))
-    (message "progargs = %s" progargs)
-    (while (not (string-equal option ""))
-      (setq progargs (cons option (cons "-I" progargs))) ;reversed
-      (message "progargs = %s" progargs)
-      (setq option (coq-ask-build-addpath-option)))
-    (message "progargs = %s" progargs)
-    (reverse progargs)))
-
-(defun coq-ask-prog-name ()
-  "Ask for and return the local variables coq-prog-name.
-These variable describes the coqtop command to be launched on this file."  
-  (let ((cmd (read-string "coq program name (default coqtop) : " "coqtop")))
-    (if (and 
-         (string-match " " cmd)
-         (not (y-or-n-p "The prog name contains spaces, are you sure? (y or n) :")))
-        (coq-ask-prog-name) ; retry
-      cmd)
-    ))
-
-
-(defun coq-ask-insert-coq-prog-name ()
-  "Ask for and insert the local variables coq-prog-name and coq-prog-args.
-These variables describe the coqtop command to be launched on this file."  
-  (interactive)
-  (let ((progname (coq-ask-prog-name))
-         (progargs (coq-ask-prog-args)))
-    (coq-insert-coq-prog-name 
-     (concat "\"" progname "\"") 
-     (concat "(\"" (proof-splice-separator "\" \"" progargs) "\")"))
-    (setq coq-prog-name progname)
-    (setq coq-prog-args progargs)))
-
-
-
 ;; ----- outline
 
 (defvar coq-outline-regexp