1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
|
;;; 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:
;;
;;; Code:
(defconst coq-local-vars-doc nil
"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.
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 *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 ((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
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 <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
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:(Emacs)File Variables)." )
(defun coq-insert-coq-prog-name (progname progargs)
"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)
;; coq-guess-command-line uses coq-prog-name, so set it
(setq coq-prog-name progname)
(setq coq-prog-args progargs))
(defun coq-read-directory (prompt &optional default maynotmatch initialcontent)
"Ask for (using PROMPT) and return a directory name.
Do not insert the default directory."
(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?? temporarily disable graphical
;; dialog, as read-file-name does not allow to select a directory
((current-use-dialog-box use-dialog-box)
(dummy (setq use-dialog-box nil))
(fname (file-name-nondirectory default))
(dir (file-name-directory default))
(path
(read-file-name prompt dir fname (not maynotmatch) initialcontent)))
(setq use-dialog-box current-use-dialog-box)
path))
;(read-file-name prompt &optional dir default-filename mustmatch
; initial predicate)
;(read-from-minibuffer
; PROMPT &optional INITIAL-CONTENTS KEYMAP READP HISTORY ABBREV-TABLE DEFAULT)
;(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
((not tl) nil)
; if the option following -I starts with '-', forget the -I :
((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.
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 (if coq-version-is-V8-1 '("-emacs-U") '("-emacs")))
(option))
;; first suggest previous directories
(while 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
(setq option (coq-read-directory
"Add directory (tab to complete, empty to stop) -I:" ""))
(while (not (string-equal option ""))
(setq progargs (cons option (cons "-I" progargs))) ;reversed
(setq option (coq-read-directory
"Add directory (tab to complete, empty to stop) -I :" "")))
(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.
Optional argument OLDVALUE specifies the previous value of `coq-prog-name', it
will be used to suggest a value to the user."
(message (concat "oldavalue: " oldvalue))
(let* ((deflt (or oldvalue "coqtop"))
(cmd (coq-read-directory
(concat "coq program name (default \"" oldvalue "\"): ")
deflt t))
(cmd (if (string-equal cmd "") oldvalue cmd)))
(if (and
(string-match " " cmd)
(not (y-or-n-p "The prog name contains spaces, are you sure ? ")))
(coq-ask-prog-name oldvalue) ; 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* ((oldname (local-vars-list-get-safe 'coq-prog-name))
(oldargs (local-vars-list-get-safe 'coq-prog-args))
(progname (coq-ask-prog-name oldname))
(progargs (coq-ask-prog-args oldargs)))
(coq-insert-coq-prog-name progname progargs)))
(provide 'coq-local-vars)
;;; coq-local-vars.el ends here
;; Local Variables: ***
;; fill-column: 79 ***
;; indent-tabs-mode: nil ***
;; End: ***
|
