Cleaning in coq and lib, fixed licenses and docstrings.

Added one or two details to docstring of generic variables.

1 files changed, 49 insertions, 44 deletions

diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 4c51b2de..5477629e 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -1,9 +1,9 @@
 ;;; coq-local-vars.el --- local variable list tools for coq
-;; Copyright (C) 1994 - 1998 LFCS Edinburgh. 
+;; Copyright (C) 1994 - 1998 LFCS Edinburgh.
 ;; Authors: Pierre Courtieu
 ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
 
-;; $Id$ 
+;; $Id$
 
 
 ;;; Commentary:
@@ -13,110 +13,114 @@
 ;;; History:
 ;; 
 
+;;; Code:
 (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
+  "Documentation-only variable.
+A very convenient way to customize file-specific variables is to use the
+File Variables (info:(Emacs)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.
+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 file by asking you some questions.  it is accessible in the menu:
 
-\"coq\"/\"set coq prog name for this file persistently\".
+\"coq\"/\"set coq prog *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).
+documentation, which explains how it is used for coq.  For more precision, refer
+to the Emacs info manual at ((Emacs)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
+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 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
+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'.
+`proof-prog-name' and <prover>-prog-args (see for example `coq-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
+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\" 
+(*
+ Local Variables:
+ coq-prog-name: \"../../coqsrc/bin/coqtop\"
  coq-prog-args: \"-emacs\" \"-I\" \"../theories\"
- compile-command: \"make -C .. -k bar/foo.vo\" 
+ 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).
-" )
+local variable (info:(Emacs)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."
+  "Insert or modify the local variables `coq-prog-name' and `coq-prog-args'.
+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)
   )
 
 
 (defun coq-read-directory (prompt)
-  "Ask for and return a directory name."
-  (let* 
+  "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-from-minibuffer 
+;(read-from-minibuffer
 ;         PROMPT &optional INITIAL-CONTENTS KEYMAP READP HISTORY ABBREV-TABLE DEFAULT)
-;(read-directory-name 
+;(read-directory-name
 ;         PROMPT &optional DIR DEFAULT MUST-MATCH INITIAL-CONTENTS HISTORY)
 
 (defun coq-extract-directories-from-args (args)
+  "Extract directory names from coq option list ARGS."
   (if (not args) ()
     (let ((hd (car args)) (tl (cdr args)))
       (cond
-       ((string-equal hd "-I") 
-	(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))) 
+	 ((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))))))
 
 
 (defun coq-ask-prog-args (&optional oldvalue)
-  "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."  
+  "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.
+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 '("-emacs"))
 	 (option))
     ;; first suggest preious directories
     (while olddirs
-      (if (y-or-n-p (format "keep the directory %s?" (car olddirs)))
+      (if (y-or-n-p (format "Keep the directory %s? " (car olddirs)))
 	  (setq progargs (cons (car olddirs) (cons "-I" progargs))))
       (setq olddirs (cdr olddirs)))
     ;; then ask for more
@@ -127,20 +131,22 @@ These variable describes the coqtop arguments to be launched on this file."
     (reverse progargs)))
 
 (defun coq-ask-prog-name (&optional oldvalue)
-  "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) : " 
+  "Ask for and return the local variables `coq-prog-name'.
+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) : "
 			  (or oldvalue "coqtop"))))
-    (if (and 
+    (if (and
          (string-match " " cmd)
-         (not (y-or-n-p "The prog name contains spaces, are you sure? (y or n) :")))
+         (not (y-or-n-p "The prog name contains spaces, are you sure ? ")))
         (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."  
+  "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* ((oldname (local-vars-list-get-safe 'coq-prog-name))
 	 (oldargs (local-vars-list-get-safe 'coq-prog-args))
@@ -154,10 +160,9 @@ These variables describe the coqtop command to be launched on this file."
 
 (provide 'coq-local-vars)
 
+;;; coq-local-vars.el ends here
 
 ;;   Local Variables: ***
 ;;   fill-column: 79 ***
 ;;   indent-tabs-mode: nil ***
 ;;   End: ***
-
-;;; coq.el ends here