diff options
| -rw-r--r-- | coq/coq-abbrev.el | 7 | ||||
| -rw-r--r-- | coq/coq.el | 62 | ||||
| -rw-r--r-- | lib/local-vars-list.el | 226 |
3 files changed, 292 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. @@ -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 diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el new file mode 100644 index 00000000..7038ebf9 --- /dev/null +++ b/lib/local-vars-list.el @@ -0,0 +1,226 @@ +;;; local-vars.el --- local variables list utilities +;; Copyright (C) 2006 Pierre Courtieu +;; Authors: Pierre Courtieu +;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + +;; This software is free software; you can redistribute it and/or +;; modify it under the terms of the GNU General Public +;; License version 2, as published by the Free Software Foundation. +;; +;; This software is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. +;; +;; See the GNU General Public License version 2 for more details +;; (enclosed in the file GPL). +;; +;; See documentation in variable holes-short-doc. +;; + +;;; Commentary: +;; See documentation in variable holes-doc. + +;;; History: +;; + +;;; Help: + +(defconst local-vars-list-doc nil + "Quoting emacs info: + +A file can contain a \"local variables list\", which specifies the values to use for +certain Emacs variables when that file is edited. See info node \"(xemacs)File +Variables\". + +local-vars-list provides two useful functions: + +\\[local-vars-list-get] that reads a local variable value at the end of the file. + +\\[local-vars-list-set] that writes a local variable value at the end of the file.") + +(defun local-vars-list-help (describe-variable 'local-vars-list-doc)) + +;;TOTO: use the code in xemacs-sources/lisp/files.el +;; in particular the function hack-local-variables-last-page + +(defun local-vars-list-insert-empty-zone () + "Insert an empty local variables zone at the end of the buffer. +Indents the zone according to mode after insertion." + (save-excursion + (goto-char (point-max)) + (let ((pt (point))) + (cond + ((not comment-start) + (insert + " +*** Local Variables: *** +*** End: *** +" + )) + + ((string-equal comment-end "") + (insert + (format + " +%s** Local Variables: *** +%s** End: *** +" + comment-start comment-start))) + + (t + (insert + (format + " +%s +*** Local Variables: *** +*** End: *** +%s" + comment-start comment-end)) + )) + (indent-region pt (point) nil) + (message "%s" "Local variables zone added at the end of the buffer.")))) + + +(defun local-vars-list-find () + "Find the local variable definition paragraph. +Return a list containing the prefix and the suffix of its first line, +or throw 'notfound if not found. Sets the point at the beginning of +the second line of the paragraph." + (goto-char (point-max)) + (catch 'notfound + (if (not (re-search-backward "Local Variables:" nil t)) (throw 'notfound nil)) + (let ((bol (save-excursion (beginning-of-line) (point))) + (eol (save-excursion (end-of-line) (point))) + (lpattern) + (rpattern)) + (setq lpattern (buffer-substring bol (point))) + (re-search-forward "Local Variables:" eol t) + (setq rpattern (buffer-substring (point) eol)) + (forward-line 1) + (beginning-of-line) + (cons lpattern (cons rpattern nil))))) + +(defun local-vars-list-goto-var (symb lpat rpat) + "Search a line defining local variable symb at current line and below. +If successful set point to the beginning of the *value* and return t. +Otherwise set point to the beginning of the last line of the local +variables list (the one containing \"End:\"), and return nil. + +lpat and rpat are the suffix and prefix of the local variable list. + +Note: this function must be called when at the beginning of a local +variable definition (or at the \"End:\" line)." + (let* ((symbname (symbol-name symb)) + (found nil) (endreached nil) + (eol)) + (while (and (not found) (not endreached)) + (setq eol (save-excursion (end-of-line) (point))) + (search-forward lpat eol) + (re-search-forward "\\([^ :]+\\):" eol) + (let ((varname (match-string 1))) + (message "varname = %s" varname) + (cond + ((string-equal varname "End") (setq endreached t) (beginning-of-line)) + ((string-equal varname symbname) (setq found t)) + (t (forward-line 1) (beginning-of-line)) + )) + (message "found %s" found) + (message "endreached %s" endreached) + ) + (if found t nil))) + + +; precond: really be on a var def line +(defun local-vars-list-get-current (lpat rpat) + "Return the value written in the local variable list at current line. + +lpat and rpat are the suffix and prefix of the local variable list. + +Note: this function must be called when at the beginning of a local +variable definition (or at the \"End:\" line)." + (let ((bol (save-excursion (beginning-of-line) (point))) + (eol (save-excursion (end-of-line) (point))) + (varname "")) + (catch 'notfound + (if (not (search-forward lpat eol t)) (throw 'notfound nil)) + (if (not (re-search-forward "\\([^ :]+\\):" eol t)) (throw 'notfound nil)) + (setq varname (match-string 1)) + (let ((boexp (point))) + (if (not (search-forward rpat eol t)) (throw 'notfound nil)) + (search-backward rpat bol) ; should always succeed + (read (buffer-substring boexp (point))))))) ; TODO: catch errors here? + + + +(defun local-vars-list-set-current (val lpat rpat) + "Write the value val in the local variable list at current line. + +lpat and rpat are the suffix and prefix of the local variable list. + +Note: this function must be called when at the beginning of a local +variable definition (or at the \"End:\" line)." + (let ((bol (save-excursion (beginning-of-line) (point))) + (eol (save-excursion (end-of-line) (point))) + (varname "")) + (search-forward lpat eol) + (re-search-forward "\\([^ :]+\\):" eol) + (setq varname (match-string 1)) + (let ((boexp (point))) + (search-forward rpat eol) + (search-backward rpat bol) + (kill-region boexp (point)) + (insert (format " %S " val)) + ) + ) + ) + + +(defun local-vars-list-get (symb) + "Return the value written in the local variable list for variable symb. +Raises an error if symb is not in the list." + (save-excursion + (let* + ((lrpat (local-vars-list-find)) + (dummy (if lrpat t (error "local variables zone not found. "))) + (lpat (car lrpat)) + (rpat (car (cdr lrpat))) + ) + (beginning-of-line) + (if (local-vars-list-goto-var symb lpat rpat) + t + (error "variable %s not found" symb)) + (beginning-of-line) + (local-vars-list-get-current lpat rpat)))) + +(defun local-vars-list-set (symb val) + "Write the value val in the local variable list for variable symb. +If the variable is already specified in the list, replace the value. If no local +variable list is found, create one at the end of the buffer first." + (save-excursion + (let ((lrpat (local-vars-list-find))) + (if (not lrpat) + (progn + (local-vars-list-insert-empty-zone) + (setq lrpat (local-vars-list-find)))) + (beginning-of-line) + (let ((lpat (car lrpat)) + (rpat (car (cdr lrpat)))) + (if (local-vars-list-goto-var symb lpat rpat) + (progn (beginning-of-line) + (local-vars-list-set-current val lpat rpat)) + (insert (format "%s%s: %S%s\n" lpat (symbol-name symb) val rpat)) + (forward-line -1) + (indent-according-to-mode)))))) + + +(provide 'local-vars-list) + + + +;;; Local Variables: *** +;;; fill-column: 85 *** +;;; indent-tabs-mode: nil *** +;;; End: *** + + + |