From b40cca6bde4d432934bdd6e38d7e7454f6e9ca5f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 17 Aug 2006 21:15:36 +0000 Subject: Moved the coq local variables tools in a separate file and made it simpler. --- coq/coq-local-vars.el | 137 ++++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 137 insertions(+) create mode 100644 coq/coq-local-vars.el (limited to 'coq/coq-local-vars.el') 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 + +;; $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 -- cgit v1.2.3