diff options
| -rw-r--r-- | coq/coq-abbrev.el | 98 | ||||
| -rw-r--r-- | coq/coq-db.el | 198 | ||||
| -rw-r--r-- | coq/coq-local-vars.el | 93 | ||||
| -rw-r--r-- | coq/coq-syntax.el | 65 | ||||
| -rw-r--r-- | coq/coq.el | 19 |
5 files changed, 263 insertions, 210 deletions
diff --git a/coq/coq-abbrev.el b/coq/coq-abbrev.el index 22fd3c19..d8a53f47 100644 --- a/coq/coq-abbrev.el +++ b/coq/coq-abbrev.el @@ -1,5 +1,8 @@ -;; default abbrev table -; This is for coq V8, you should test coq version before loading +;;; coq-abbrev.el --- coq abbrev table and menus for ProofGeneral mode +;; Copyright (C) 1994 - 1998 LFCS Edinburgh. +;; Authors: Healfdene Goguen, Pierre Courtieu +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> (require 'proof) (require 'coq-syntax) @@ -13,86 +16,6 @@ (describe-variable 'coq-local-vars-doc)) - -;; Computes the max length of strings in a list -(defun max-length-db (db) - (let ((l db) (res 0)) - (while l - (let ((lgth (length (car (car l))))) - (setq res (max lgth res)) - (setq l (cdr l)))) - res)) - - - -(defun coq-build-menu-from-db-internal (db lgth menuwidth) - "Take a keyword database DB and return insertion menus for them." - (let ((l db) (res ()) (size lgth) - (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) - (while (and l (> size 0)) - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - (e6 (car-safe tl5)) ; e6 = function for smart insertion - (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu - (entry-with (max (- menuwidth (length e1)) 0)) - (spaces (make-string entry-with ? )) - ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) - ) - (when (not e7) ; if not hidden - (let ((menu-entry - (vector - ;; menu entry label - (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) - ;;insertion function if present otherwise insert completion - (if e6 e6 `(holes-insert-and-expand ,e3)) - t))) - (setq res (nconc res (list menu-entry)))));; append *in place* - (setq l tl) - (setq size (- size 1)))) - res)) - - -(defun coq-build-title-menu (l size) - (concat (car-safe (car-safe l)) - " ... " - (car-safe (car-safe (nthcdr (- size 1) l))))) - - -(defun coq-build-menu-from-db (db &optional size) - "Take a keyword database DB and return a list of insertion menus for - them. -Submenus contain SIZE entries (default 30)." - (let* ((l db) (res ()) - (wdth (+ 2 (max-length-db coq-tactics-db))) - (sz (or size 30)) (lgth (length l))) - (while l - (if (<= lgth sz) - (setq res - (nconc res (list (cons (coq-build-title-menu l lgth) - (coq-build-menu-from-db-internal l lgth wdth))))) - (setq res - (nconc res (list (cons (coq-build-title-menu l sz) - (coq-build-menu-from-db-internal l sz wdth)))))) - (setq l (nthcdr sz l)) - (setq lgth (length l))) - res)) - -(defun coq-build-abbrev-table-from-db (db) - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - ) - (when e2 (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) - (setq l tl))) - res)) - (defconst coq-tactics-menu (append '("INSERT TACTICS" ["Intros (smart)" coq-insert-intros t]) @@ -119,11 +42,9 @@ Submenus contain SIZE entries (default 30)." (defconst coq-commands-abbrev-table (coq-build-abbrev-table-from-db coq-commands-db)) - - (defconst coq-terms-menu (append '("INSERT TERM" - ["Match!" coq-insert-match t]) + ["Match (smart)" coq-insert-match t]) (coq-build-menu-from-db coq-terms-db))) (defconst coq-terms-abbrev-table @@ -219,14 +140,15 @@ Submenus contain SIZE entries (default 30)." ;; 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] - ["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t] + ["Set coq prog *persistently*" coq-ask-insert-coq-prog-name t] + ["help on setting persistently" coq-local-vars-list-show-doc t] )) ;; da: Moved this from the main menu to the Help submenu. ;; It also appears under Holes, anyway. (defpgdefault help-menu-entries - '(["Tell me about holes?" holes-show-doc t])) + '(["Tell me about holes?" holes-show-doc t] + ["help on setting prog name persistently for a file" coq-local-vars-list-show-doc t])) (provide 'coq-abbrev) diff --git a/coq/coq-db.el b/coq/coq-db.el new file mode 100644 index 00000000..cd350a22 --- /dev/null +++ b/coq/coq-db.el @@ -0,0 +1,198 @@ +;;; coq-db.el --- coq keywords database utility functions +;; Copyright (C) 1997, 1998 LFCS Edinburgh. +;; Authors: Thomas Kleymann and Healfdene Goguen +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Pierre Courtieu <courtieu@lri.fr> + + +;;; We store all information on keywords (tactics or command) in big +;; tables (ex: `coq-tactics-db') From there we get: menus including +;; "smart" commands, completions for command coq-insert-... +;; abbrev tables and font-lock keyword + +;;; real value defined below + +;;; Commentary: +;; + +;;; Code: +(defconst coq-syntax-db nil + "Documentation-only variable, for coq keyword databases. +Each element of a keyword database contains the definition of a \"form\", of the +form: + +(MENUNAME ABBREV INSERT STATECH KWREG INSERT-FUN HIDE) + +MENUNAME is the name of form (or form variant) as it should appear in menus or +completion lists. + +ABBREV is the abbreviation for completion via `expand-abbrev'. + +INSERT is the complete text of the form, which may contain holes denoted by +\"#\" or \"@{xxx}\". + +If non-nil the optional STATECH specifies that the command is not state +preserving for coq. + +If non-nil the optional KWREG is the regexp to colorize correponding to the +keyword. ex: \"simple\\\\s-+destruct\" + +If non-nil the optional INSERT-FUN is the function to be called when inserting +the form (instead of inserting INSERT, except when using `expand-abbrev'). This +allows to write functions asking for more information to assist the user. + +If non-nil the optional HIDE specifies that this form should not appear in the +menu but only in completions." ) + +(defun coq-insert-from-db (db) + "Ask for a keyword, with completion on keyword database DB and insert. +Insert corresponding string with holes at point. If an insertion function is +present for the keyword, call it instead. see `coq-syntax-db' for DB +structure." + (let* ((tac (completing-read "tactic (tab for completion) : " + db nil nil)) + (infos (cddr (assoc tac db))) + (s (car infos)) ; completion to insert + (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function + (pt (point))) + (if f (funcall f) ; call f if present + (insert (or s tac)) ; insert completion and indent otherwise + (holes-replace-string-by-holes-backward-jump pt) + (indent-according-to-mode)))) + + + +(defun coq-build-regexp-list-from-db (db &optional filter) + "Take a keyword database DB and return the list of regexps for font-lock. +If non-nil Optional argument FILTER is a function applying to each line of DB. +For each line if FILTER returns nil, then the keyword is not added to the +regexp. See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l))(tl (cdr l)) ; hd is the first infos list + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing + (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string + ) + ;; TODO delete doublons + (when (and e5 (or (not filter) (funcall filter hd))) + (setq res (nconc res (list e5)))) + (setq l tl))) + res + )) + +;; Computes the max length of strings in a list +(defun max-length-db (db) + "Return the length of the longest first element (menu label) of DB. +See `coq-syntax-db' for DB structure." + (let ((l db) (res 0)) + (while l + (let ((lgth (length (car (car l))))) + (setq res (max lgth res)) + (setq l (cdr l)))) + res)) + + + +(defun coq-build-menu-from-db-internal (db lgth menuwidth) + "Take a keyword database DB and return one insertion submenu. +Argument LGTH is the max size of the submenu. Argument MENUWIDTH is the width +of the largest line in the menu (without abbrev and shortcut specifications). +Used by `coq-build-menu-from-db', which you should probably use instead. See +`coq-syntax-db' for DB structure." + (let ((l db) (res ()) (size lgth) + (keybind-abbrev (substitute-command-keys " \\[expand-abbrev]"))) + (while (and l (> size 0)) + (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing + (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string + (e6 (car-safe tl5)) ; e6 = function for smart insertion + (e7 (car-safe (cdr-safe tl5))) ; e7 = if non-nil : hide in menu + (entry-with (max (- menuwidth (length e1)) 0)) + (spaces (make-string entry-with ? )) + ;;(restofmenu (coq-build-menu-from-db-internal tl (- size 1) menuwidth)) + ) + (when (not e7) ; if not hidden + (let ((menu-entry + (vector + ;; menu entry label + (concat e1 (if (not e2) "" (concat spaces "(" e2 keybind-abbrev ")"))) + ;;insertion function if present otherwise insert completion + (if e6 e6 `(holes-insert-and-expand ,e3)) + t))) + (setq res (nconc res (list menu-entry)))));; append *in place* + (setq l tl) + (setq size (- size 1)))) + res)) + + +(defun coq-build-title-menu (db size) + "Build a title for the first submenu of DB, of size SIZE. +Return the string made of the first and the SIZE nth first element of DB, +separated by \"...\". Used by `coq-build-menu-from-db'. See `coq-syntax-db' +for DB structure." + (concat (car-safe (car-safe db)) + " ... " + (car-safe (car-safe (nthcdr (- size 1) db))))) + + +(defun coq-build-menu-from-db (db &optional size) + "Take a keyword database DB and return a list of insertion menus for them. +Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB +structure." + (let* ((l db) (res + ()) + (wdth (+ 2 (max-length-db coq-tactics-db))) + (sz (or size 30)) (lgth (length l))) + (while l + (if (<= lgth sz) + (setq res + (nconc res (list (cons (coq-build-title-menu l lgth) + (coq-build-menu-from-db-internal l lgth wdth))))) + (setq res + (nconc res (list (cons (coq-build-title-menu l sz) + (coq-build-menu-from-db-internal l sz wdth)))))) + (setq l (nthcdr sz l)) + (setq lgth (length l))) + res)) + +(defun coq-build-abbrev-table-from-db (db) + "Take a keyword database DB and return an abbrev table. +See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l))(tl (cdr l)) ; hd is a list of length 3 or 4 + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + ) + (when e2 (setq res (nconc res (list `(,e2 ,e3 holes-abbrev-complete))))) + (setq l tl))) + res)) + + +(defun filter-state-preserving (l) + ; checkdoc-params: (l) + "Not documented." + (not (nth 3 l))) ; fourth argument is nil --> state preserving command + +(defun filter-state-changing (l) + ; checkdoc-params: (l) + "Not documented." + (nth 3 l)) ; fourth argument is nil --> state preserving command + + + +(provide 'coq-db) +(provide 'coq-db) + +;;; coq-db.el ends here + +;** Local Variables: *** +;** fill-column: 80 *** +;** End: *** 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 diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el index 267e5a95..090a4374 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1,11 +1,13 @@ ;; coq-syntax.el Font lock expressions for Coq ;; Copyright (C) 1997, 1998 LFCS Edinburgh. ;; Authors: Thomas Kleymann and Healfdene Goguen +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <courtieu@lri.fr> ;; $Id$ (require 'proof-syntax) +(require 'coq-db) ;; da 15/2/03: without defvars compilation breaks ;; This may have broken some of logic below @@ -68,67 +70,6 @@ version of coq by doing 'coqtop -v'." ) ;;; keyword databases -;;; We store all information on keywords (tactics or command) in big -;;; tables (ex: `coq-tactics-db') From there we get: menus including -;;; "smart" commands, completions for command coq-insert-... -;;; abbrev tables and font-lock keyword - -;;; real value defined below -(defconst coq-syntax-db nil - "This variable is only used for documentation for lists of keyword -information lists, like for example `coq-user-tactics-db'. Each -element is a list of the form - -(MENUNAME ABBREVIATION COMPLETION STATE-CHANGE TO-COLORIZE INSERTION-FUN HIDE-IN-MENU) - -MENUNAME is the name of tactic (or tactic variant) as it should -appear in menus. - -ABBREVIATION is the abbreviation for completion via `expand-abbrev'. - -COMPLETION is the complete text of the tactic, which may contain holes -denoted by \"#\" or \"@{}\". - -If non-nil the optional STATE-CHANGE specifies that the command is not -state preserving for coq. - -If non-nil the optional TO-COLORIZE is the regexp to colorize -correponding to this tactic. ex: \"simple\\\\s-+destruct\" - -If non-nil the optional INSERTION-FUN is the function to be called -when inserting the tactic. This allows to ask for more information to -assist tactic writing. This function is not called when using -completion, it is used when using menu or `coq-insert-tactic'. - -If non-nil the optional HIDE-IN-MENU specifies that this tactic should -not appear in the menu but only in when calling `coq-insert-tactic'." ) - - - -(defun coq-build-regexp-list-from-db (db &optional filter) - "Take a keyword database L and return the list of regexps for font-lock." - (let ((l db) (res ())) - (while l - (let* ((hd (car l))(tl (cdr l)) ; hd is the first infos list - (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry - (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation - (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion - (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing - (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string - ) - ;; TODO delete doublons - (when (and e5 (or (not filter) (funcall filter hd))) - (setq res (nconc res (list e5)))) - (setq l tl))) - res - )) - -(defun filter-state-preserving (l) - (not (nth 3 l))) ; fourth argument is nil --> state preserving command - -(defun filter-state-changing (l) - (nth 3 l)) ; fourth argument is nil --> state preserving command - (defcustom coq-user-tactics-db nil "User defined tactic information. See `coq-syntax-db' for @@ -324,7 +265,7 @@ so for the following reasons: ("idtac" nil "idtac") ; also in tactics ; ("idtac \"" nil "idtac \"#\"") ; also in tactics ("fail" "fa" "fail" nil "fail") - ("fail \"" "fa\"" "fail" nil) +; ("fail \"" "fa\"" "fail" nil) ; ; ("orelse" nil "orelse #" t "orelse") ("repeat" nil "repeat #" nil "repeat") ("try" nil "try #" nil "try") @@ -1,6 +1,7 @@ ;;; coq.el --- Major mode for Coq proof assistant ;; Copyright (C) 1994 - 1998 LFCS Edinburgh. ;; Authors: Healfdene Goguen, Pierre Courtieu +;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> ;; $Id$ @@ -30,13 +31,14 @@ ;; On Windows with latest Coq package you might need something like: ;; "C:/Program Files/Coq/bin/coqtop.opt.exe" ;; instead of just "coqtop". See also coq-prog-env below. - "*Name of program to run as Coq." + "*Name of program to run as Coq. Important: See `proof-prog-name'." :type 'string :group 'coq) ;; List of arguments to pass to Coq process. Should contain -emacs. ;; -translate will be added automatically to this list if `coq-translate-to-v8' ;; is set. +;; coq-prog-args is set by defpgcustom in proof-config (setq coq-prog-args '("-emacs")) ;; List of environment settings d to pass to Coq process. @@ -1328,21 +1330,6 @@ positions." ))))) -(defun coq-insert-from-db (db) - "Ask for a keyword, with completion on list DB tactics and insert -corresponding string with holes at point. If a insertion function is presnet -for the keyword, call it instead." - (let* ((tac (completing-read "tactic (tab for completion) : " - db nil nil)) - (infos (cddr (assoc tac db))) - (s (car infos)) ; completion to insert - (f (car-safe (cdr-safe (cdr-safe (cdr infos))))) ; insertion function - (pt (point))) - (if f (funcall f) ; call f if present - (insert (or s tac)) ; insert completion and indent otherwise - (holes-replace-string-by-holes-backward-jump pt) - (indent-according-to-mode)))) - (defun coq-insert-tactic () "Ask for a tactic name, with completion on a quasi-exhaustive list of coq |