diff options
Diffstat (limited to 'coq')
| -rw-r--r-- | coq/coq-autotest.el | 5 | ||||
| -rw-r--r-- | coq/coq-compile-common.el | 5 | ||||
| -rw-r--r-- | coq/coq-db.el | 19 | ||||
| -rw-r--r-- | coq/coq-local-vars.el | 7 | ||||
| -rw-r--r-- | coq/coq-par-compile.el | 3 | ||||
| -rw-r--r-- | coq/coq-seq-compile.el | 3 | ||||
| -rw-r--r-- | coq/coq-system.el | 8 | ||||
| -rw-r--r-- | coq/coq.el | 53 |
8 files changed, 42 insertions, 61 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index cecfdcf1..8be4bed9 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -3,7 +3,7 @@ ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -16,9 +16,6 @@ ;;; Code: -(eval-when-compile - (require 'cl)) - (require 'pg-autotest) (require 'proof-site) diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el index 9dca0082..d29bf1b9 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -22,6 +22,7 @@ ;;; Code: +(require 'cl-lib) ;cl-every cl-some (require 'proof-shell) (require 'coq-system) (require 'compile) @@ -442,7 +443,7 @@ expressions in here are always matched against the .vo file name, regardless whether ``-quick'' would be used to compile the file or not." :type '(repeat regexp) - :safe (lambda (v) (every 'stringp v)) + :safe (lambda (v) (cl-every #'stringp v)) :group 'coq-auto-compile) (defcustom coq-coqdep-error-regexp @@ -531,7 +532,7 @@ for instance, not make sense to let ProofGeneral check if the coq standard library is up-to-date. This function is always invoked on the .vo file name, regardless whether the file would be compiled with ``-quick'' or not." - (if (some + (if (cl-some (lambda (dir-regexp) (string-match dir-regexp lib-obj-file)) coq-compile-ignored-directories) (progn diff --git a/coq/coq-db.el b/coq/coq-db.el index cad149a2..36812c4c 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -1,9 +1,9 @@ -;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; -*- +;;; coq-db.el --- coq keywords database utility functions -*- coding: utf-8; lexical-binding:t -*- ;; This file is part of Proof General. ;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh -;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc. +;; Portions © Copyright 2003-2018 Free Software Foundation, Inc. ;; Portions © Copyright 2001-2017 Pierre Courtieu ;; Portions © Copyright 2010, 2016 Erik Martin-Dorel ;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews @@ -23,8 +23,7 @@ ;;; Code: -(eval-when-compile - (require 'cl)) +(eval-when-compile (require 'cl-lib)) ;decf (require 'proof-config) ; for proof-face-specs, a macro (require 'proof-syntax) ; for proof-ids-to-regexp @@ -95,7 +94,7 @@ the first hole even if more than one." -(defun coq-build-command-from-db (db prompt &optional preformatquery) +(defun coq-build-command-from-db (db prompt &optional _preformatquery) "Ask for a keyword, with completion on keyword database DB and send to Coq. See `coq-syntax-db' for DB structure." ;; Next invocation of minibuffer (read-string below) will first recursively @@ -192,8 +191,8 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See (menu (nth 0 hd)) ; e1 = menu entry (abbrev (nth 1 hd)) ; e2 = abbreviation (complt (nth 2 hd)) ; e3 = completion - (state (nth 3 hd)) ; e4 = state changing - (color (nth 4 hd)) ; e5 = colorization string + ;; (state (nth 3 hd)) ; e4 = state changing + ;; (color (nth 4 hd)) ; e5 = colorization string (insertfn (nth 5 hd)) ; e6 = function for smart insertion (menuhide (nth 6 hd)) ; e7 = if non-nil : hide in menu (entry-with (max (- menuwidth (length menu)) 0)) @@ -212,7 +211,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See t))) (setq res (nconc res (list menu-entry)))));; append *in place* (setq l (cdr l)) - (decf size))) + (cl-decf size))) res)) @@ -264,9 +263,9 @@ 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 + (_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 + (e3 (car tl2)) (_tl3 (cdr tl2)) ; e3 = completion ) ;; careful: nconc destructive! (when e2 diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index f172adbe..2211c22d 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -1,4 +1,4 @@ -;;; coq-local-vars.el --- local variable list tools for coq +;;; coq-local-vars.el --- local variable list tools for coq -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -19,9 +19,6 @@ (require 'local-vars-list) ; in lib directory -(eval-when-compile - (require 'cl)) - (defvar coq-prog-name) (defvar coq-load-path) @@ -136,7 +133,7 @@ Do not insert the default directory." ;; 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)) + (_dummy (setq use-dialog-box nil)) (fname (file-name-nondirectory default)) (dir (file-name-directory default)) (path diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index b03fedaa..c6822dc5 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.el @@ -34,9 +34,6 @@ ;;; Code: -(eval-when-compile - (require 'proof-compat)) - (defvar queueitems) ; dynamic scope in p-s-extend-queue-hook (require 'coq-compile-common) diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 74327b53..4889ccaf 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.el @@ -24,9 +24,6 @@ ;;; Code: -(eval-when-compile - (require 'proof-compat)) - (defvar queueitems) ; dynamic scope in p-s-extend-queue-hook (require 'coq-compile-common) diff --git a/coq/coq-system.el b/coq/coq-system.el index bb1c28f0..bd0f7eba 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -1,4 +1,4 @@ -;;; coq-system.el --- common part of compilation feature +;;; coq-system.el --- common part of compilation feature -*- lexical-binding:t -*- ;; This file is part of Proof General. @@ -25,10 +25,6 @@ (require 'proof) -(eval-when-compile - (require 'cl) - (require 'proof-compat)) - (defvar coq-prog-args) (defvar coq-debug) @@ -514,7 +510,7 @@ coqtop." (`("-arg" ,concatenated-args) (setq args (append args - (split-string-and-unquote (cadr opt) coq--project-file-separator)))))) + (split-string-and-unquote concatenated-args coq--project-file-separator)))))) (cons "-emacs" args))) (defun coq--extract-load-path-1 (option base-directory) @@ -19,10 +19,9 @@ ;;; Code: -(eval-when-compile - (require 'cl) - (require 'proof-compat)) +(require 'cl-lib) +(require 'span) (eval-when-compile (require 'proof-utils) (require 'span) @@ -37,10 +36,10 @@ (defvar old-proof-marker) (defvar coq-keymap) (defvar coq-one-command-per-line) -(defvar coq-auto-insert-as) ; defpacustom -(defvar coq-time-commands) ; defpacustom -(defvar coq-use-project-file) ; defpacustom -(defvar coq-use-editing-holes) ; defpacustom +(defvar coq-auto-insert-as) ; defpacustom +(defvar coq-time-commands) ; defpacustom +(defvar coq-use-project-file) ; defpacustom +(defvar coq-use-editing-holes) ; defpacustom (defvar coq-hide-additional-subgoals) (require 'proof) @@ -1585,7 +1584,7 @@ of hypothesis to highlight." See `coq-highlight-hyps-cited-in-response' and `SearchAbout'." (let* ((hyps-cited-pos (coq-detect-hyps-positions proof-response-buffer)) (hyps-cited (coq-build-hyps-names hyps-cited-pos))) - (remove-if-not + (cl-remove-if-not (lambda (e) (cl-some;seq-find (lambda (f) @@ -2536,7 +2535,7 @@ mouse activation." (defun coq-directories-files (l) (let* ((file-list-list (mapcar 'directory-files l)) (file-list (apply 'append file-list-list)) - (filtered-list (remove-if-not 'coq-postfix-.v-p file-list))) + (filtered-list (cl-remove-if-not #'coq-postfix-.v-p file-list))) filtered-list)) (defun coq-remove-dot-v-extension (s) @@ -2547,8 +2546,8 @@ mouse activation." (defun coq-build-accessible-modules-list () (let* ((pth (or coq-load-path '("."))) - (cleanpth (mapcar 'coq-load-path-to-paths pth)) - (existingpth (remove-if-not 'file-exists-p cleanpth)) + (cleanpth (mapcar #'coq-load-path-to-paths pth)) + (existingpth (cl-remove-if-not #'file-exists-p cleanpth)) (file-list (coq-directories-files existingpth))) (mapcar 'coq-remove-dot-v-extension file-list))) @@ -2586,11 +2585,11 @@ mouse activation." (completing-read "Command (TAB to see list, default Require Import) : " reqkinds-kinds-table nil nil nil nil "Require Import"))) - (loop do - (setq s (completing-read "Name (empty to stop) : " - (coq-build-accessible-modules-list))) - (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s))) - while (not (string-equal s ""))))) + (cl-loop do + (setq s (completing-read "Name (empty to stop) : " + (coq-build-accessible-modules-list))) + (unless (zerop (length s)) (insert (format "%s %s.\n" reqkind s))) + while (not (string-equal s ""))))) ;; TODO add module closing (defun coq-end-Section () @@ -2731,16 +2730,16 @@ Also insert holes at insertion positions." (insert match) (indent-region start (point) nil) (let ((n (holes-replace-string-by-holes-backward start))) - (case n - (0 nil) ; no hole, stay here. - (1 - (goto-char start) - (holes-set-point-next-hole-destroy)) ; if only one hole, go to it. - (t - (goto-char start) - (message - (substitute-command-keys - "\\[holes-set-point-next-hole-destroy] to jump to active hole. \\[holes-short-doc] to see holes doc.")))))))))) + (pcase n + (0 nil) ; no hole, stay here. + (1 + (goto-char start) + (holes-set-point-next-hole-destroy)) ; if only one hole, go to it. + (_ + (goto-char start) + (message + (substitute-command-keys + "\\[holes-set-point-next-hole-destroy] to jump to active hole. \\[holes-short-doc] to see holes doc.")))))))))) (defun coq-insert-solve-tactic () "Ask for a closing tactic name, with completion, and insert at point. @@ -3318,8 +3317,6 @@ priority to the former." (provide 'coq) - - ;; Local Variables: *** ;; fill-column: 79 *** ;; indent-tabs-mode: nil *** |