continue on the support for local variables list semi-automatic

insertion. I put a new file in lib with basic tools for file variables
lists.

2 files changed, 66 insertions, 3 deletions

diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el
index ae21a1fb..19b2ac44 100644
--- a/coq/coq-abbrev.el
+++ b/coq/coq-abbrev.el
@@ -5,6 +5,10 @@
   (interactive)
   (describe-variable 'holes-doc))
 
+(defun coq-local-vars-list-show-doc ()
+  (interactive)
+  (describe-variable 'coq-local-vars-doc))
+
 ;#s and @{..} are replaced by holes by holes-abbrev-complete
 (if (boundp 'holes-abbrev-complete)
 	 ()
@@ -390,7 +394,8 @@
     ;; With all these submenus you have to wonder if these things belong
     ;; on the main menu.  Are they the most often used?
     ["Compile" coq-Compile t]
-    ["Set coq prog name for this file persistently" coq-ask-insert-coq-prog-name t]
+    ["Set coq prog name *for this file persistently*" coq-ask-insert-coq-prog-name t]
+    ["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t]
     ))
 
 ;; da: Moved this from the main menu to the Help submenu.  
diff --git a/coq/coq.el b/coq/coq.el
index 3e4f9660..bb4c10fb 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -15,6 +15,7 @@
 
 (require 'proof)
 (require 'holes-load) ; in lib directory
+(require 'local-vars-list) ; in lib directory
 ;; coq-syntaxe is required below
 ;; ----- coq-shell configuration options
 
@@ -181,6 +182,63 @@ 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)
@@ -1412,8 +1470,8 @@ mouse activation."
 (provide 'coq)
 
 ;;   Local Variables: ***
-;;   fill-column: 85 ***
-;;   indent-tabs-mode:nil ***
+;;   fill-column: 79 ***
+;;   indent-tabs-mode: nil ***
 ;;   End: ***
 
 ;;; coq.el ends here