diff options
Diffstat (limited to 'coq')
-rw-r--r-- | coq/coq-autotest.el | 5 | ||||
-rw-r--r-- | coq/coq-compile-common.el | 14 | ||||
-rw-r--r-- | coq/coq-db.el | 19 | ||||
-rw-r--r-- | coq/coq-indent.el | 5 | ||||
-rw-r--r-- | coq/coq-local-vars.el | 14 | ||||
-rw-r--r-- | coq/coq-par-compile.el | 8 | ||||
-rw-r--r-- | coq/coq-seq-compile.el | 8 | ||||
-rw-r--r-- | coq/coq-system.el | 15 | ||||
-rw-r--r-- | coq/coq.el | 117 |
9 files changed, 87 insertions, 118 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 97ea6ec6..d29bf1b9 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.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 @@ -22,14 +22,14 @@ ;;; Code: +(require 'cl-lib) ;cl-every cl-some (require 'proof-shell) (require 'coq-system) (require 'compile) -(eval-when-compile - ;;(defvar coq-pre-v85 nil) - (defvar coq-confirm-external-compilation); defpacustom - (defvar coq-compile-parallel-in-background)) ; defpacustom +;;(defvar coq-pre-v85 nil) +(defvar coq-confirm-external-compilation); defpacustom +(defvar coq-compile-parallel-in-background) ; defpacustom ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; @@ -443,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 @@ -532,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-indent.el b/coq/coq-indent.el index 6e8ba013..af780251 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.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 @@ -33,8 +33,7 @@ ; ,@body ; (message "%.06f" (float-time (time-since time))))) -(eval-when-compile - (defvar coq-script-indent)) +(defvar coq-script-indent) (defconst coq-any-command-regexp (proof-regexp-alt-list coq-keywords)) diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index b8c5d7e3..2211c22d 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 +;;; coq-local-vars.el --- local variable list tools for coq -*- 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 @@ -19,12 +19,8 @@ (require 'local-vars-list) ; in lib directory -(eval-when-compile - (require 'cl)) - -(eval-when-compile - (defvar coq-prog-name) - (defvar coq-load-path)) +(defvar coq-prog-name) +(defvar coq-load-path) (defconst coq-local-vars-doc nil @@ -137,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 e3daebcd..c6822dc5 100644 --- a/coq/coq-par-compile.el +++ b/coq/coq-par-compile.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 @@ -34,11 +34,7 @@ ;;; Code: -(eval-when-compile - (require 'proof-compat)) - -(eval-when-compile - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook +(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 5875908c..4889ccaf 100644 --- a/coq/coq-seq-compile.el +++ b/coq/coq-seq-compile.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 @@ -24,11 +24,7 @@ ;;; Code: -(eval-when-compile - (require 'proof-compat)) - -(eval-when-compile - (defvar queueitems)) ; dynamic scope in p-s-extend-queue-hook +(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 308a4599..28c73ae7 100644 --- a/coq/coq-system.el +++ b/coq/coq-system.el @@ -1,9 +1,9 @@ -;;; 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. ;; 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 @@ -25,13 +25,8 @@ (require 'proof) -(eval-when-compile - (require 'cl) - (require 'proof-compat)) - -(eval-when-compile - (defvar coq-prog-args) - (defvar coq-debug)) +(defvar coq-prog-args) +(defvar coq-debug) ;; Arbitrary arguments can already be passed through _CoqProject. ;; However this is not true for all assistants, so we don't modify the @@ -529,7 +524,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) @@ -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 @@ -19,30 +19,28 @@ ;;; Code: -(eval-when-compile - (require 'cl) - (require 'proof-compat)) +(require 'cl-lib) +(require 'span) (eval-when-compile (require 'proof-utils) (require 'span) (require 'outline) (require 'newcomment) - (require 'etags) - (unless (proof-try-require 'smie) - (defvar smie-indent-basic) - (defvar smie-rules-function)) - (defvar proof-info) ; dynamic scope in proof-tree-urgent-action - (defvar action) ; dynamic scope in coq-insert-as stuff - (defvar string) ; dynamic scope in coq-insert-as stuff - (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-hide-additional-subgoals)) + (require 'etags)) +(defvar smie-indent-basic) +(defvar smie-rules-function) +(defvar proof-info) ; dynamic scope in proof-tree-urgent-action +(defvar action) ; dynamic scope in coq-insert-as stuff +(defvar string) ; dynamic scope in coq-insert-as stuff +(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-hide-additional-subgoals) (require 'proof) (require 'coq-system) ; load path, option, project file etc. @@ -66,11 +64,8 @@ ;; prettify is in emacs > 24.4 ;; FIXME: this should probably be done like for smie above. -(defvar coq-may-use-prettify nil) ; may become t below -(eval-when-compile - (if (fboundp 'prettify-symbols-mode) - (defvar coq-may-use-prettify t) - (defvar prettify-symbols-alist nil))) +(defvar coq-may-use-prettify (fboundp 'prettify-symbols-mode)) +(defvar prettify-symbols-alist) ;; ----- coq-shell configuration options @@ -911,22 +906,21 @@ This is mapped to control/shift mouse-1, unless coq-remap-mouse-1 is nil (t by default)." (interactive "e") (save-selected-window - (save-selected-frame - (save-excursion - (mouse-set-point event) - (let* ((id (coq-id-at-point)) - (notat (coq-notation-at-position (point))) - (modifs (event-modifiers event)) - (shft (member 'shift modifs)) - (ctrl (member 'control modifs)) - (cmd (when (or id notat) - (if (and ctrl shft) (if id "Check" "Locate") - (if shft (if id "About" "Locate") - (if ctrl (if id "Print" "Locate"))))))) - (proof-shell-invisible-command - (format (concat cmd " %s . ") - ;; Notation need to be surrounded by "" - (if id id (concat "\"" notat "\""))))))))) + (save-excursion + (mouse-set-point event) + (let* ((id (coq-id-at-point)) + (notat (coq-notation-at-position (point))) + (modifs (event-modifiers event)) + (shft (member 'shift modifs)) + (ctrl (member 'control modifs)) + (cmd (when (or id notat) + (if (and ctrl shft) (if id "Check" "Locate") + (if shft (if id "About" "Locate") + (if ctrl (if id "Print" "Locate"))))))) + (proof-shell-invisible-command + (format (concat cmd " %s . ") + ;; Notation need to be surrounded by "" + (if id id (concat "\"" notat "\"")))))))) (defun coq-guess-or-ask-for-string (s &optional dontguess) "Asks for a coq identifier with message S. @@ -1211,8 +1205,7 @@ Printing All set." (coq-ask-do-show-all "Show goal number" "Show" t)) ;; Check -(eval-when-compile - (defvar coq-auto-adapt-printing-width)); defpacustom +(defvar coq-auto-adapt-printing-width); defpacustom ;; Since Printing Width is a synchronized option in coq (?) it is retored ;; silently to a previous value when retracting. So we reset the stored width @@ -1591,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) @@ -2542,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) @@ -2553,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))) @@ -2592,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 () @@ -2737,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. @@ -3324,8 +3317,6 @@ priority to the former." (provide 'coq) - - ;; Local Variables: *** ;; fill-column: 79 *** ;; indent-tabs-mode: nil *** |