diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-12-14 15:44:32 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2018-12-14 15:44:32 +0100 |
| commit | ed4ffd4a653ae792aefeacbb0daa967fd4cb2524 (patch) | |
| tree | 60a407c7f8ee7f2eb7a0dfd21230f47b1295d6b1 | |
| parent | bfcb1a442b225394edc5e61ff8b3216e8f0efe83 (diff) | |
| parent | 632a3d7f9ded16faaf58e1c0769bcd4f7c8193e3 (diff) | |
Merge branch 'master' of github.com:ProofGeneral/PG
47 files changed, 357 insertions, 505 deletions
@@ -2,5 +2,6 @@ nohup.out TAGS ChangeLog +proof-general-autoloads.el *.elc *~ 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 *** diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el index 409fd22a..2943dd9f 100644 --- a/doc/docstring-magic.el +++ b/doc/docstring-magic.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 @@ -23,7 +23,6 @@ (append '("../generic/") load-path)) (load "proof-site.el") (require 'proof-autoloads) -(require 'proof-compat) (require 'proof-utils) diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index e9b40358..621805e7 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -10,6 +10,7 @@ ;;; Commentary: ;; +(require 'cl-lib) ;cl-every (require 'proof) (require 'easycrypt-syntax) (require 'easycrypt-hooks) @@ -24,7 +25,7 @@ (defun easycrypt-load-path-safep (path) (and (listp path) - (every (lambda (entry) (stringp entry)) path))) + (cl-every #'stringp path))) ;; -------------------------------------------------------------------- (defcustom easycrypt-prog-name "easycrypt" diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el index b06b4ec5..59593ad6 100644 --- a/generic/pg-assoc.el +++ b/generic/pg-assoc.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 @@ -21,6 +21,7 @@ ;;; Code: +(require 'cl-lib) ;cl-remove-if-not (require 'proof-utils) (define-derived-mode proof-universal-keys-only-mode fundamental-mode @@ -66,13 +67,13 @@ argument ALL-FRAMES has the same meaning than for (defun proof-filter-associated-windows (lw) "Remove windows of LW not displaying at least one associated buffer." - (remove-if-not (lambda (w) (proof-associated-buffer-p (window-buffer w))) lw)) + (cl-remove-if-not (lambda (w) (proof-associated-buffer-p (window-buffer w))) lw)) ;;;###autoload (defun proof-associated-frames () "Return the list of frames displaying at least one associated buffer." - (remove-if-not (lambda (f) (proof-filter-associated-windows (window-list f))) + (cl-remove-if-not (lambda (f) (proof-filter-associated-windows (window-list f))) (frame-list))) (provide 'pg-assoc) diff --git a/generic/pg-goals.el b/generic/pg-goals.el index baab5561..d9a350ec 100644 --- a/generic/pg-goals.el +++ b/generic/pg-goals.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 @@ -19,10 +19,9 @@ ;;; Code: (eval-when-compile (require 'easymenu) ; easy-menu-add, etc - (require 'cl) ; incf - (require 'span) ; span-* - (defvar proof-goals-mode-menu) ; defined by macro below - (defvar proof-assistant-menu)) ; defined by macro in proof-menu + (require 'span)) ; span-* +(defvar proof-goals-mode-menu) ; defined by macro below +(defvar proof-assistant-menu) ; defined by macro in proof-menu (require 'pg-assoc) diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el index 0f427ecb..e84061b8 100644 --- a/generic/pg-pgip.el +++ b/generic/pg-pgip.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,7 +33,7 @@ ;; ;;; Code: -(require 'cl) ; incf +(require 'cl-lib) ; incf (require 'pg-xml) ; (declare-function pg-response-warning "pg-response") @@ -55,8 +55,8 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe ;; PGIP processing is split into two steps: ;; (1) process each command, altering internal data structures ;; (2) post-process for each command type, affecting external interface (menus, etc). - (mapc 'pg-pgip-post-process - (reduce 'union (mapcar 'pg-pgip-process-pgip pgips)))) + (mapc #'pg-pgip-post-process + (cl-reduce #'cl-union (mapcar #'pg-pgip-process-pgip pgips)))) ;; TODO: use id's and sequence numbers to reconstruct streams of messages. (defvar pg-pgip-last-seen-id nil) @@ -78,7 +78,7 @@ The list PGIPS may contain one or more PGIP packets, whose contents are processe (setq pg-pgip-last-seen-seq seq) (if (eq name 'pgip) ;; NB: schema currently allows only one message here - (mapcar 'pg-pgip-process-msg (xml-node-children pgip)) + (mapcar #'pg-pgip-process-msg (xml-node-children pgip)) (pg-internal-warning "pg-pgip-process-pgip: expected PGIP element, got %s" name)))) (defun pg-pgip-process-msg (pgipmsg) @@ -246,7 +246,7 @@ Return a symbol representing the PGIP command processed, or nil." (dolist (idtable idtables) (let* ((context (pg-xml-get-attr 'context idtable 'optional)) (objtype (intern (pg-pgip-get-objtype idtable))) - (idents (mapcar 'pg-xml-get-text-content + (idents (mapcar #'pg-xml-get-text-content (xml-get-children idtable 'identifier))) (obarray (or (and (not (eq opn 'setids)) (get objtype 'pgsymbols)) @@ -255,7 +255,7 @@ Return a symbol representing the PGIP command processed, or nil." (setq proof-assistant-idtables (if (and (null idents) (eq opn 'setids)) (delete objtype proof-assistant-idtables) - (adjoin objtype proof-assistant-idtables))) + (cl-adjoin objtype proof-assistant-idtables))) (cond ((or (eq opn 'setids) (eq opn 'addids)) (mapc (lambda (i) (intern i obarray)) idents)) @@ -400,7 +400,7 @@ Also sets local proverid and srcid variables for buffer." (with-current-buffer buffer (make-local-variable 'proverid) (setq proverid proverid)) - (set pg-pgip-srcids (acons srcid (list buffer file) pg-pgip-srcids))))) + (set pg-pgip-srcids (cl-acons srcid (list buffer file) pg-pgip-srcids))))) ;; FIXME: right action? @@ -483,7 +483,7 @@ Also sets local proverid and srcid variables for buffer." (list 'const val)))) ((eq tyname 'pgipchoice) (let* ((choicesnodes (pg-xml-child-elts node)) - (choices (mapcar 'pg-pgip-get-pgiptype choicesnodes))) + (choices (mapcar #'pg-pgip-get-pgiptype choicesnodes))) (list 'choice choices))) (t (pg-pgip-warning "pg-pgip-get-pgiptype: unrecognized/missing typename \"%s\"" tyname))))) @@ -605,7 +605,7 @@ OTHERCLASS overrides this." "/" proof-assistant))) (id (pg-xml-attr id pg-pgip-id)) (class (pg-xml-attr class (or otherclass "pa"))) - (seq (pg-xml-attr seq (int-to-string (incf pg-pgip-seq)))) + (seq (pg-xml-attr seq (int-to-string (cl-incf pg-pgip-seq)))) (refseq (if refseq (list (pg-xml-attr refseq refseq)))) (refid (if refid (list (pg-xml-attr refid refid)))) (pgip_attrs (append (list tag id class seq) diff --git a/generic/pg-response.el b/generic/pg-response.el index 43e0e279..650e83a0 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.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,9 +24,9 @@ (eval-when-compile (require 'easymenu) ; easy-menu-add - (require 'proof-utils) ; deflocal, proof-eval-when-ready-for-assistant - (defvar proof-response-mode-menu nil) - (defvar proof-assistant-menu nil)) + (require 'proof-utils)) ; deflocal, proof-eval-when-ready-for-assistant +(defvar proof-response-mode-menu) +(defvar proof-assistant-menu) (require 'pg-assoc) (require 'span) diff --git a/generic/pg-user.el b/generic/pg-user.el index 126901cb..a5ed27a9 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -1,9 +1,9 @@ -;;; pg-user.el --- User level commands for Proof General +;;; pg-user.el --- User level commands for Proof General -*- 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 @@ -26,9 +26,7 @@ (require 'proof-script) ; we build on proof-script -(require 'cl) -(eval-when-compile - (require 'completion)) ; Loaded dynamically at runtime. +(eval-when-compile (require 'cl-lib)) ;cl-decf (defvar which-func-modes) ; Defined by which-func. (declare-function proof-segment-up-to "proof-script") @@ -557,26 +555,29 @@ Uses `add-completion' with a negative number of uses and ancient last use time, to discourage saving these into the users database." (interactive) (require 'completion) + (defvar completion-min-length) + (declare-function add-completion "completion" + (string &optional num-uses last-use-time)) (mapcar (lambda (cmpl) ;; completion gives error; trapping is tricky so test again (if (>= (length cmpl) completion-min-length) (add-completion cmpl -1000 0))) (proof-ass completion-table))) -;; completion not autoloaded in GNU Emacs -(or (fboundp 'complete) - (autoload 'complete "completion")) - ;; NB: completion table is expected to be set when proof-script ;; is loaded! Call `proof-script-add-completions' to update. -(unless (bound-and-true-p byte-compile-current-file) +(unless (bound-and-true-p byte-compile-current-file) ;FIXME: Yuck! (eval-after-load "completion" '(proof-add-completions))) (defun proof-script-complete (&optional arg) - "Like `complete' but case-fold-search set to proof-case-fold-search." + "Like `complete' but case-fold-search set to `proof-case-fold-search'." (interactive "*p") + ;; completion not autoloaded in GNU Emacs + ;; FIXME: It's probably because we shouldn't use it ;-) + (require 'completion) + (declare-function complete "completion" (&optional arg)) (let ((case-fold-search proof-case-fold-search)) (complete arg))) @@ -863,10 +864,9 @@ The function `substitute-command-keys' is called on the argument." (interactive "e") (if proof-query-identifier-command (save-selected-window - (save-selected-frame - (save-excursion - (mouse-set-point event) - (pg-identifier-near-point-query)))))) + (save-excursion + (mouse-set-point event) + (pg-identifier-near-point-query))))) ;;;###autoload (defun pg-identifier-near-point-query () @@ -890,13 +890,12 @@ a popup with the information in it." (pg-identifier-query identifier ctxt ;; the callback - (lexical-let ((s start) (e end)) - (lambda (x) - (save-excursion - (let ((idspan (span-make s e))) - ;; (span-set-property idspan 'priority 90) ; highest - (span-set-property idspan 'help-echo - (pg-last-output-displayform)))))))))) + (lambda (_) + (save-excursion + (let ((idspan (span-make start end))) + ;; (span-set-property idspan 'priority 90) ; highest + (span-set-property idspan 'help-echo + (pg-last-output-displayform))))))))) (defvar proof-query-identifier-history nil "History for `proof-query-identifier'.") @@ -1254,7 +1253,7 @@ the locked region." (while (> repeat 0) (pg-protected-undo-1 newarg) ; do some safe undos step by step (setq last-command 'undo) ; need for this assignment meanwhile - (decf repeat))))) + (cl-decf repeat))))) (defun pg-protected-undo-1 (arg) "This function is intended to be called by `pg-protected-undo'. diff --git a/generic/pg-xml.el b/generic/pg-xml.el index 18285572..4e5ea385 100644 --- a/generic/pg-xml.el +++ b/generic/pg-xml.el @@ -1,9 +1,9 @@ -;;; pg-xml.el --- XML functions for Proof General +;;; pg-xml.el --- XML functions for Proof General -*- 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 @@ -20,8 +20,7 @@ ;;; Code: -(require 'cl) - +(require 'cl-lib) ;cl-mapcan (require 'xml) (require 'proof-utils) ;; for pg-internal-warning @@ -90,7 +89,7 @@ Optional START and END bound the parse." (defun pg-xml-child-elts (node) "Return list of *element* children of NODE (ignoring strings)." (let ((children (xml-node-children node))) - (mapcan (lambda (x) (if (listp x) (list x))) children))) + (cl-mapcan (lambda (x) (if (listp x) (list x))) children))) (defun pg-xml-child-elt (node) "Return unique element child of NODE." @@ -134,10 +133,10 @@ Optional START and END bound the parse." "Convert the XML trees in XMLS into a string (without additional indentation)." (let* (strs (insertfn (lambda (&rest args) - (setq strs (cons (reduce 'concat args) strs))))) + (push (mapconcat #'identity args "") strs)))) (dolist (xml xmls) (pg-xml-output-internal xml nil insertfn)) - (reduce 'concat (reverse strs)))) + (mapconcat #'identity (reverse strs) ""))) ;; based on xml-debug-print from xml.el @@ -187,7 +186,7 @@ Cal OUTPUTFN, which should accept a list of args." (defsubst pg-pgip-get-area (node &optional optional defaultval) (pg-xml-get-attr 'area node optional defaultval)) -(defun pg-pgip-get-icon (node &optional optional defaultval) +(defun pg-pgip-get-icon (node &optional _optional _defaultval) "Return the <icon> child of NODE, or nil if none." (pg-xml-get-child 'icon node)) diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el index 083f42f3..5d2a18cd 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -14,8 +14,6 @@ ;;; Code: -(eval-when-compile - (require 'cl)) (eval-when-compile (require 'pg-vars) diff --git a/generic/proof-depends.el b/generic/proof-depends.el index 72beb1d2..9f3b469a 100644 --- a/generic/proof-depends.el +++ b/generic/proof-depends.el @@ -1,9 +1,9 @@ -;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies +;;; proof-depends.el --- Theorem-theorem and theorem-definition dependencies -*- 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,7 +23,7 @@ ;; ;;; Code: -(require 'cl) +(require 'cl-lib) (require 'span) (require 'pg-vars) (require 'proof-config) @@ -191,12 +191,11 @@ Called from `proof-done-advancing' when a save is processed and (subitems (and ns (assoc ns nested)))) (cond ((and ns subitems) - (setcdr subitems (adjoin name (cdr subitems)))) + (setcdr subitems (cl-adjoin name (cdr subitems)))) (ns - (setq nested - (cons (cons ns (list name)) nested))) + (push (cons ns (list name)) nested)) (t - (setq toplevel (adjoin name toplevel)))))) + (setq toplevel (cl-adjoin name toplevel)))))) (cons nested toplevel))) (defun proof-dep-make-submenu (name namefn appfn list) @@ -221,7 +220,7 @@ NAMEFN is applied to each element of LIST to make the names." ;; Functions triggered by menus ;; -(defun proof-goto-dependency (name span) +(defun proof-goto-dependency (_name span) "Go to the start of SPAN." ;; FIXME(EMD): seems buggy as NAME is not used ;; FIXME: check buffer is right one. Later we'll allow switching buffer diff --git a/generic/proof-maths-menu.el b/generic/proof-maths-menu.el index b1155557..6ff81c90 100644 --- a/generic/proof-maths-menu.el +++ b/generic/proof-maths-menu.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 @@ -27,9 +27,6 @@ ;;; Code: (eval-when-compile - (require 'cl)) - -(eval-when-compile (require 'proof-auxmodes) ; loaded by proof.el (require 'maths-menu)) ; loaded dynamically in proof-auxmodes diff --git a/generic/proof-menu.el b/generic/proof-menu.el index fc18d504..e43efcc0 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.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 @@ -17,11 +17,10 @@ ;; ;;; Code: -(require 'cl) ; mapcan +(require 'cl-lib) ; cl-mapcan, ... -(eval-when-compile - (defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific - (defvar proof-mode-map)) +(defvar proof-assistant-menu) ; defined by macro in proof-menu-define-specific +(defvar proof-mode-map) (require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant (require 'proof-useropts) @@ -50,24 +49,26 @@ without adjusting window layout." (cond ((and (called-interactively-p 'any) (eq last-command 'proof-display-some-buffers)) - (incf proof-display-some-buffers-count)) + (cl-incf proof-display-some-buffers-count)) (t (setq proof-display-some-buffers-count 0))) - (let* ((assocbufs (remove-if-not 'buffer-live-p - (list proof-response-buffer - proof-thms-buffer - proof-trace-buffer - proof-goals-buffer - ))) + (let* ((assocbufs (cl-remove-if-not #'buffer-live-p + (list proof-response-buffer + proof-thms-buffer + proof-trace-buffer + proof-goals-buffer + ))) ;proof-shell-buffer (numassoc (length assocbufs))) ;; If there's no live other buffers, we don't do anything. (unless (zerop numassoc) (let ((selectedbuf (nth (mod proof-display-some-buffers-count - numassoc) assocbufs)) + numassoc) + assocbufs)) (nextbuf (nth (mod (1+ proof-display-some-buffers-count) - numassoc) assocbufs))) + numassoc) + assocbufs))) (cond ((or proof-three-window-enable proof-multiple-frames-enable) ;; Display two buffers: next in rotation and goals/response @@ -75,7 +76,8 @@ without adjusting window layout." (proof-switch-to-buffer selectedbuf 'noselect) (proof-switch-to-buffer (if (eq selectedbuf proof-goals-buffer) proof-response-buffer - proof-goals-buffer) 'noselect)) + proof-goals-buffer) + 'noselect)) (selectedbuf (proof-switch-to-buffer selectedbuf 'noselect))) (if (eq selectedbuf proof-response-buffer) @@ -756,7 +758,7 @@ suitable for adding to the proof assistant menu." (while (and new (fboundp menu-fn)) (setq menu-fn (intern (concat (symbol-name menuname-sym) "-" (int-to-string i)))) - (incf i)) + (cl-incf i)) (if inscript (eval `(proof-defshortcut ,menu-fn ,command ,key)) (eval `(proof-definvisible ,menu-fn ,command ,key))) @@ -790,7 +792,7 @@ suitable for adding to the proof assistant menu." nil t))) (let* ((favs (proof-ass favourites)) - (rmfavs (remove-if + (rmfavs (cl-remove-if (lambda (f) (string-equal menuname (caddr f))) favs))) (unless (equal favs rmfavs) @@ -832,7 +834,7 @@ KEY is the optional key binding." (let* ((menu-entry (proof-def-favourite command inscript menuname key t)) (favs (proof-ass favourites)) - (rmfavs (remove-if + (rmfavs (cl-remove-if (lambda (f) (string-equal menuname (caddr f))) favs)) (newfavs (append @@ -861,7 +863,7 @@ KEY is the optional key binding." (mapc (lambda (stg) (add-to-list 'groups (get (car stg) 'pggroup))) proof-assistant-settings) (dolist (grp (reverse groups)) - (let* ((gstgs (mapcan (lambda (stg) + (let* ((gstgs (cl-mapcan (lambda (stg) (if (eq (get (car stg) 'pggroup) grp) (list stg))) proof-assistant-settings)) diff --git a/generic/proof-script.el b/generic/proof-script.el index c938dfad..4c56fc7b 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.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,15 +24,15 @@ ;;; Code: -(require 'cl) ; various +(require 'cl-lib) ; various (require 'span) ; abstraction of overlays/extents (require 'proof-utils) ; proof-utils macros (require 'proof-syntax) ; utils for manipulating syntax (eval-when-compile - (require 'easymenu) - (defvar proof-mode-menu nil) - (defvar proof-assistant-menu nil)) + (require 'easymenu)) +(defvar proof-mode-menu) +(defvar proof-assistant-menu) (declare-function proof-shell-strip-output-markup "proof-shell" (string &optional push)) @@ -520,8 +520,8 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'." (defun pg-get-element (idiomsym id) "Return proof script element of type IDIOMSYM with identifier ID. IDIOMSYM is a symbol, ID is a string." - (assert (symbolp idiomsym)) - (assert (stringp id)) + (cl-assert (symbolp idiomsym)) + (cl-assert (stringp id)) (let ((idsym (intern id)) (elts (cdr-safe (assq idiomsym pg-script-portions)))) (if elts @@ -539,9 +539,9 @@ NAME does not need to be unique. NAME is a name that comes from the proof script or prover output. It is recorded in the span with the 'rawname property." - (assert (symbolp idiomsym)) - (assert (stringp id)) - (if name (assert (stringp name))) + (cl-assert (symbolp idiomsym)) + (cl-assert (stringp id)) + (if name (cl-assert (stringp name))) (let* ((idsym (intern id)) (rawname name) (name (or name id)) @@ -880,8 +880,8 @@ proof assistant and Emacs has a modified buffer visiting the file." (funcall proof-shell-inform-file-retracted-cmd rfile) (proof-restart-buffers (proof-files-to-buffers - (set-difference current-included - proof-included-files-list))))))) + (cl-set-difference current-included + proof-included-files-list))))))) (defun proof-auto-retract-dependencies (cfile &optional informprover) "Perhaps automatically retract the (linear) dependencies of CFILE. @@ -1234,8 +1234,8 @@ activation is considered to have failed and an error is given." ;; proof-unregister-buffer-file-name. (if proof-script-buffer (proof-deactivate-scripting)) - (assert (null proof-script-buffer) - "Bug in proof-activate-scripting: deactivate failed.") + (cl-assert (null proof-script-buffer) + "Bug in proof-activate-scripting: deactivate failed.") ;; Set the active scripting buffer (setq proof-script-buffer (current-buffer)) @@ -1340,7 +1340,7 @@ Argument SPAN has just been processed." ;; CASE 2: Save command seen, now we may amalgamate spans. ((and (proof-string-match-safe proof-save-command-regexp cmd) (funcall proof-really-save-command-p span cmd) - (decf proof-nesting-depth) ;; [always non-nil/true] + (cl-decf proof-nesting-depth) ;; [always non-nil/true] (if proof-nested-goals-history-p ;; For now, we only support this nesting behaviour: ;; don't amalgamate unless the nesting depth is 0, @@ -1479,15 +1479,15 @@ Argument SPAN has just been processed." ((and proof-nested-goals-history-p proof-save-command-regexp (proof-string-match proof-save-command-regexp cmd)) - (incf lev)) + (cl-incf lev)) ;; Decrement depth when a goal is hit ((funcall proof-goal-command-p gspan) - (decf lev)) + (cl-decf lev)) ;; Remainder cases: see if command matches something we ;; should count for a global undo ((and proof-nested-undo-regexp (proof-string-match proof-nested-undo-regexp cmd)) - (incf nestedundos)) + (cl-incf nestedundos)) )))) (if (not gspan) @@ -1556,7 +1556,7 @@ Subroutine of `proof-done-advancing-save'." ;; In the extend case, the context of proof grows until hit a save ;; or new goal. (if (eq proof-completed-proof-behaviour 'extend) - (incf proof-shell-proof-completed) + (cl-incf proof-shell-proof-completed) (setq proof-shell-proof-completed nil)) (let* ((swallow (eq proof-completed-proof-behaviour 'extend)) @@ -1623,12 +1623,12 @@ Subroutine of `proof-done-advancing-save'." (cond ((funcall proof-goal-command-p span) (pg-add-element 'statement id bodyspan) - (incf proof-nesting-depth)) + (cl-incf proof-nesting-depth)) (t (pg-add-element 'command id bodyspan))) (if proof-shell-proof-completed - (incf proof-shell-proof-completed)) + (cl-incf proof-shell-proof-completed)) (pg-set-span-helphighlights span proof-command-mouse-highlight-face))) @@ -1969,7 +1969,7 @@ We assume that the list is contiguous and begins at (proof-queue-or-locked-end). We also delete help spans which appear in the same region (in the expectation that these may be overwritten). This function expects the buffer to be activated for advancing." - (assert semis nil "proof-assert-semis: argument must be a list") + (cl-assert semis nil "proof-assert-semis: argument must be a list") (let ((startpos (proof-queue-or-locked-end)) (lastpos (nth 2 (car semis))) (vanillas (proof-semis-to-vanillas semis displayflags))) @@ -2458,13 +2458,13 @@ For this function to work properly, you must configure (setq str (span-property span 'cmd)) (cond ((eq (span-property span 'type) 'vanilla) (unless (proof-stringfn-match proof-ignore-for-undo-count str) - (incf ct))) + (cl-incf ct))) ((eq (span-property span 'type) 'pbp) (setq i 0) (while (< i (length str)) (if (string-equal (substring str i (+ i tl)) proof-terminal-string) - (incf ct)) - (incf i)))) + (cl-incf ct)) + (cl-incf i)))) (setq span (next-span span 'type))) (if (= ct 0) nil ; was proof-no-command diff --git a/generic/proof-shell.el b/generic/proof-shell.el index b5bbcd9f..a176283d 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1,9 +1,9 @@ -;;; proof-shell.el --- Proof General shell mode. +;;; proof-shell.el --- Proof General shell mode ;; 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,7 +22,7 @@ ;;; Code: -(require 'cl) ; set-difference, every +(require 'cl-lib) ; cl-set-difference, cl-every (eval-when-compile (require 'span) @@ -34,15 +34,14 @@ (declare-function proof-tree-urgent-action "proof-tree" (flags)) (declare-function proof-tree-handle-delayed-output "proof-tree" (old-proof-marker cmd flags span)) -(eval-when-compile - ;; without the nil initialization the compiler still warns about this variable - (defvar proof-tree-external-display nil)) +;; without the nil initialization the compiler still warns about this variable +(defvar proof-tree-external-display) (require 'scomint) (require 'pg-response) (require 'pg-goals) (require 'pg-user) ; proof-script, new-command-advance - +(require 'span) ;; ;; Internal variables used by proof shell @@ -454,8 +453,7 @@ process command." ;; Call multiple-frames-enable in case we need to fire up ;; new frames (NB: sets specifiers to remove modeline) (save-selected-window - (save-selected-frame - (proof-multiple-frames-enable))))) + (proof-multiple-frames-enable)))) (message "Starting %s process... done." proc)))) @@ -506,7 +504,7 @@ shell buffer, called by `proof-shell-bail-out' if process exits." (while (and (> timecount 0) (scomint-check-proc proof-shell-buffer)) (accept-process-output proc 1 nil 1) - (decf timecount))) + (cl-decf timecount))) ;; Still there, kill it rudely. (when (memq (process-status proc) '(open run stop)) @@ -892,7 +890,7 @@ inserted text. Do not use this function directly, or output will be lost. It is only used in `proof-add-to-queue' when we start processing a queue, and in `proof-shell-exec-loop', to process the next item." - (assert (or (stringp strings) + (cl-assert (or (stringp strings) (listp strings)) nil "proof-shell-insert: expected string list argument") @@ -1010,7 +1008,7 @@ being processed." (unless (eq proof-shell-busy queuemode) (proof-debug "proof-append-alist: wrong queuemode detected for busy shell") - (assert (eq proof-shell-busy queuemode))))) + (cl-assert (eq proof-shell-busy queuemode))))) (let ((nothingthere (null proof-action-list))) @@ -1184,7 +1182,7 @@ contains only invisible elements for Prooftree synchronization." (and (not proof-second-action-list-active) (or (null proof-action-list) - (every + (cl-every (lambda (item) (memq 'proof-tree-show-subgoal (nth 3 item))) proof-action-list))))))) @@ -1312,8 +1310,8 @@ to `proof-register-possibly-new-processed-file'." ;; the proof-shell-compute-new-files-list (proof-restart-buffers (proof-files-to-buffers - (set-difference current-included - proof-included-files-list))) + (cl-set-difference current-included + proof-included-files-list))) (cond ;; Do nothing if there was no active scripting buffer ((not scrbuf)) @@ -1764,7 +1762,7 @@ Only works when system timer has microsecond count available." (and (< (- tm pg-last-tracing-output-time) (/ pg-fast-tracing-mode-threshold 1000000.0)) - (>= (incf pg-last-trace-output-count) + (>= (cl-incf pg-last-trace-output-count) pg-slow-mode-trigger-count)) ;; quickly consecutive tracing outputs: go into slow mode (setq dontprint t) @@ -1858,16 +1856,14 @@ The flag 'invisible is always added to FLAGS." (not proof-shell-auto-terminate-commands) (string-match (concat (regexp-quote proof-terminal-string) - "[ \t]*$") cmd)) + "[ \t]*$") + cmd)) (setq cmd (concat cmd proof-terminal-string))) (if wait (proof-shell-wait)) (proof-shell-ready-prover) ; start proof assistant; set vars. (let* ((callback - (if invisiblecallback - (lexical-let ((icb invisiblecallback)) - (lambda (span) - (funcall icb span))) - 'proof-done-invisible))) + (or invisiblecallback + #'proof-done-invisible))) (proof-start-queue nil nil (list (proof-shell-action-list-item cmd diff --git a/generic/proof-site.el b/generic/proof-site.el index e339d022..fd48002f 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.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 @@ -169,8 +169,7 @@ You can use customize to set this variable." (require 'pg-vars) (require 'proof-autoloads) -(eval-when-compile - (defvar Info-dir-contents)) +(defvar Info-dir-contents) ;; Add the info directory to the Info path (if (file-exists-p proof-info-directory) ; for safety diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 5871a993..e93f5ca4 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.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 @@ -20,7 +20,6 @@ ;;; Code: (require 'font-lock) (require 'proof-config) ; proof-case-fold-search -(require 'proof-compat) ; proof-buffer-syntactic-context (require 'pg-pamacs) ; proof-ass-sym (defsubst proof-ids-to-regexp (l) diff --git a/generic/proof-tree.el b/generic/proof-tree.el index cb85952d..c7afe212 100644 --- a/generic/proof-tree.el +++ b/generic/proof-tree.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 @@ -93,8 +93,7 @@ ;;; Code: -(require 'cl) - +(eval-when-compile (require 'cl-lib)) ;cl-assert (eval-when-compile (require 'proof-shell)) @@ -622,7 +621,7 @@ primitives is changed.") Send a message with command line SECOND-LINE and all strings in DATA as data sections to Prooftree." (let ((second-line-len (string-bytes second-line))) - (assert (< second-line-len 999)) + (cl-assert (< second-line-len 999)) (process-send-string proof-tree-process (format "second line %03d\n%s\n%s%s" @@ -1157,7 +1156,7 @@ entry that is now finally retired. CMD is the command, FLAGS are the flags and SPAN is the span." ;; (message "PTHDO cmd %s flags %s span %s-%s" cmd flags ;; (if span (span-start span)) (if span (span-end span))) - (assert proof-tree-external-display) + (cl-assert proof-tree-external-display) (unless (or (memq 'invisible flags) (memq 'proof-tree-show-subgoal flags)) (let* ((proof-info (funcall proof-tree-get-proof-info)) (current-proof-name (cadr proof-info))) @@ -1226,7 +1225,7 @@ position of the current proof." (error "Enabling prooftree inside a proof outside the current scripting buffer")) (proof-shell-ready-prover) - (assert proof-locked-span) + (cl-assert proof-locked-span) (message "Start proof-tree display for current proof") (save-excursion (save-window-excursion diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el index 2deca0e6..7ae75ba1 100644 --- a/generic/proof-unicode-tokens.el +++ b/generic/proof-unicode-tokens.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 @@ -25,9 +25,6 @@ ;;; Code: (eval-when-compile - (require 'cl)) - -(eval-when-compile (require 'scomint) (require 'proof-auxmodes) ; loaded by proof.el, autoloads us (require 'unicode-tokens)) ; it will be loaded by proof-auxmodes diff --git a/generic/proof-utils.el b/generic/proof-utils.el index b4e7e0d1..99e537c5 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.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 @@ -40,7 +40,7 @@ (if (or (not (boundp 'emacs-major-version)) (< emacs-major-version 23) - (string-match "XEmacs" emacs-version)) + (featurep 'xemacs)) (error "Proof General is not compatible with Emacs %s" emacs-version)) (unless (equal pg-compiled-for (pg-emacs-version-cookie)) @@ -51,7 +51,6 @@ (require 'proof-site) ; basic vars -(require 'proof-compat) ; compatibility (require 'pg-pamacs) ; macros for pa config (require 'proof-config) ; config vars (require 'bufhist) ; bufhist @@ -399,8 +398,9 @@ or if the window is the only window of its frame." (select-window window)))) ;; the window is the full width, right? ;; [if not, we may be in horiz-split scheme, problematic] - (not (window-leftmost-p window)) - (not (window-rightmost-p window))) + (not (zerop (car (window-edges window)))) ;not leftmost + (not (>= (nth 2 (window-edges window)) ;not rightmost + (frame-width (window-frame window))))) ;; OK, we're not going to adjust the height here. Moreover, ;; we'll make sure the height can be changed elsewhere. (setq window-size-fixed nil) diff --git a/generic/proof.el b/generic/proof.el index 5fa9de33..f3b3b276 100644 --- a/generic/proof.el +++ b/generic/proof.el @@ -1,9 +1,9 @@ -;;; proof.el --- Proof General theorem prover interface. +;;; proof.el --- Proof General theorem prover interface ;; 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 @@ -36,7 +36,6 @@ (unless (or noninteractive (bound-and-true-p byte-compile-current-file)) (proof-splash-message)) ; welcome the user now. -(require 'proof-compat) ; Emacs and OS compatibility (require 'proof-utils) ; utilities (require 'proof-config) ; configuration variables (require 'proof-auxmodes) ; auxmode functions diff --git a/hol-light/hol-light-autotest.el b/hol-light/hol-light-autotest.el index d68b898f..dab2c4c4 100644 --- a/hol-light/hol-light-autotest.el +++ b/hol-light/hol-light-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, 2012, 2014, 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 'proof-site) (proof-ready-for-assistant 'hol-light) diff --git a/hol-light/hol-light.el b/hol-light/hol-light.el index 2b4f3989..808e04a9 100644 --- a/hol-light/hol-light.el +++ b/hol-light/hol-light.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,12 +22,10 @@ (require 'proof-easy-config) ; easy configure mechanism (require 'proof-syntax) ; functions for making regexps -(or (proof-try-require 'caml-font) ; use OCaml Emacs mode syntax - (defvar caml-font-lock-keywords nil)) ; +(proof-try-require 'caml-font) ; use OCaml Emacs mode syntax (eval-when-compile - (require 'proof-tree) - (defvar caml-font-lock-keywords nil)) + (require 'proof-tree)) (defcustom hol-light-home (or (getenv "HOLLIGHT_HOME") @@ -317,7 +315,7 @@ You need to restart Emacs if you change this setting." proof-script-font-lock-keywords (append - caml-font-lock-keywords + (bound-and-true-p caml-font-lock-keywords) (list (cons (proof-ids-to-regexp hol-light-keywords) 'font-lock-keyword-face) (cons (proof-ids-to-regexp hol-light-tactics) 'proof-tactics-name-face) diff --git a/isar/isabelle-system.el b/isar/isabelle-system.el index e399474b..4fb2bcde 100644 --- a/isar/isabelle-system.el +++ b/isar/isabelle-system.el @@ -1,6 +1,7 @@ ;; isabelle-system.el --- Interface with Isabelle system ;; ;; Copyright (C) 2000 LFCS Edinburgh, David Aspinall. +;; Copyright (C) 2018 Free Software Foundation, Inc. ;; ;; Author: David Aspinall <da@dcs.ed.ac.uk> ;; Maintainer: Proof General maintainer <proofgen@dcs.ed.ac.uk> @@ -12,16 +13,15 @@ ;; ;;; Code: -(eval-when-compile - (require 'cl)) ; mapcan, eval-when +(require 'cl-lib) ;cl-mapcan (eval-when-compile (require 'span) (require 'scomint) (require 'proof-site) (require 'proof-menu) - (require 'proof-syntax) - (defvar proof-assistant-menu)) + (require 'proof-syntax)) +(defvar proof-assistant-menu) (declare-function mapcan "cl-extra") ; spurious bytecomp warning @@ -233,7 +233,7 @@ passed to isa-tool-doc-command, DOCNAME will be viewed." (let ((docs (isa-shell-command-to-string (concat "\"" isa-isabelle-command "\" doc")))) (unless (string-equal docs "") - (mapcan + (cl-mapcan (function (lambda (docdes) (if (proof-string-match "^[ \t]+\\(\\S-+\\)[ \t]+" docdes) (list (list diff --git a/isar/isar-autotest.el b/isar/isar-autotest.el index f8784bc2..8e098a29 100644 --- a/isar/isar-autotest.el +++ b/isar/isar-autotest.el @@ -10,9 +10,6 @@ (require 'pg-autotest) -(eval-when-compile - (require 'cl)) - (require 'proof-site) (proof-ready-for-assistant 'isar) diff --git a/isar/isar-profiling.el b/isar/isar-profiling.el index 0cf19348..ae8a8f8c 100644 --- a/isar/isar-profiling.el +++ b/isar/isar-profiling.el @@ -5,9 +5,6 @@ ;; $Id$ ;; -(eval-when-compile - (require 'cl)) - (require 'proof-site) (proof-ready-for-assistant 'isar) diff --git a/isar/isar-syntax.el b/isar/isar-syntax.el index 7fa6f55d..095b108c 100644 --- a/isar/isar-syntax.el +++ b/isar/isar-syntax.el @@ -8,7 +8,7 @@ ;; $Id$ ;; -(require 'cl) ; remove-if, remove-if-not +(eval-when-compile (require 'cl-lib)) (require 'proof-syntax) (require 'isar-keywords) ; NB: we want to load isar-keywords at runtime @@ -271,18 +271,18 @@ matches contents of quotes for quoted identifiers.") (while (proof-re-search-forward isar-nesting-regexp limit t) (cond ((proof-buffer-syntactic-context)) - ((equal (match-string 0) isar-keyword-begin) (incf nesting)) - ((equal (match-string 0) isar-keyword-end) (decf nesting))))) + ((equal (match-string 0) isar-keyword-begin) (cl-incf nesting)) + ((equal (match-string 0) isar-keyword-end) (cl-decf nesting))))) nesting)) (defun isar-match-nesting (limit) - (block nil + (cl-block nil (while (proof-re-search-forward isar-nesting-regexp limit t) (and (not (proof-buffer-syntactic-context)) (if (equal (match-string 0) isar-keyword-begin) (> (isar-nesting) 1) (> (isar-nesting) 0)) - (return t))))) + (cl-return t))))) ;; ----- Isabelle inner syntax highlight diff --git a/isar/isar-unicode-tokens.el b/isar/isar-unicode-tokens.el index c6f58452..725bc544 100644 --- a/isar/isar-unicode-tokens.el +++ b/isar/isar-unicode-tokens.el @@ -12,7 +12,7 @@ ;; -(require 'cl) ; for-loop +(eval-when-compile (require 'cl-lib)) ; cl-loop (eval-when-compile (require 'unicode-tokens) ; it's loaded dynamically at runtime @@ -481,10 +481,10 @@ tokens." :set 'isar-set-and-restart-tokens) (defun isar-map-letters (f1 f2 &rest symbs) - (loop for x below 26 - for c = (+ 65 x) - collect - (cons (funcall f1 c) (cons (funcall f2 c) symbs)))) + (cl-loop for x below 26 + for c = (+ 65 x) + collect + (cons (funcall f1 c) (cons (funcall f2 c) symbs)))) (defconst isar-script-letters-tokens ; \<A> \<B> ... (isar-map-letters (lambda (x) (format "%c" x)) diff --git a/isar/isar.el b/isar/isar.el index bb755d4f..9deed7c1 100644 --- a/isar/isar.el +++ b/isar/isar.el @@ -1,6 +1,7 @@ ;; isar.el --- Major mode for Isabelle/Isar proof assistant ;; ;; Copyright (C) 1994-2010 LFCS Edinburgh. +;; Copyright (C) 2018 Free Software Foundation, Inc. ;; ;; License: GPL (GNU GENERAL PUBLIC LICENSE) ;; @@ -16,18 +17,15 @@ ;;; Code: -(eval-when-compile - (require 'cl)) - (eval-when-compile (require 'span) (require 'proof-syntax) (require 'pg-goals) (require 'pg-vars) - (require 'outline) - (defvar comment-quote-nested) - (defvar isar-use-find-theorems-form) - (defvar isar-use-linear-undo)) + (require 'outline)) +(defvar comment-quote-nested) +(defvar isar-use-find-theorems-form) +(defvar isar-use-linear-undo) (require 'proof) (require 'isabelle-system) ; system code diff --git a/lego/lego.el b/lego/lego.el index 29564c87..248e9d09 100644 --- a/lego/lego.el +++ b/lego/lego.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 @@ -19,6 +19,7 @@ ;;; Code: +(require 'cl-lib) ;cl-member-if (require 'proof) (require 'lego-syntax) (eval-when-compile @@ -376,7 +377,7 @@ Value for `proof-shell-compute-new-files-list', which see. For LEGO, we assume that module identifiers coincide with file names." (let ((module (match-string 1))) - (cdr (member-if + (cdr (cl-member-if (lambda (filename) (lego-equal-module-filename module filename)) proof-included-files-list)))) diff --git a/lib/holes.el b/lib/holes.el index 9a45037c..84dcf1f3 100644 --- a/lib/holes.el +++ b/lib/holes.el @@ -1,9 +1,9 @@ -;;; holes.el --- a little piece of elisp to define holes in your buffer +;;; holes.el --- a little piece of elisp to define holes in your buffer -*- 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 @@ -36,7 +36,7 @@ ;;; Code: (require 'span) -(require 'cl) +(eval-when-compile (require 'cl-lib)) ;;; ;;; initialization @@ -65,16 +65,14 @@ and this is this one. This is not buffer local.") (defcustom holes-empty-hole-string "#" "String to be inserted for empty hole (don't put an empty string)." - :type 'string - :group 'holes) + :type 'string) (defcustom holes-empty-hole-regexp "#\\|@{\\([^{}]*\\)}" "Regexp denoting a hole in abbrevs. Subgroup 1 is treated specially: if it matches, it is assumed that everything before it and after it in the regexp matches delimiters which should be removed when making the text into a hole." - :type 'regexp - :group 'holes) + :type 'regexp) ;(defcustom holes-search-limit 1000 @@ -97,8 +95,7 @@ which should be removed when making the text into a hole." :background "darkred" :foreground "white") (((class color) (background light)) :background "paleVioletRed" :foreground "black")) - "Font Lock face used to highlight the active hole." - :group 'holes) + "Font Lock face used to highlight the active hole.") (defface inactive-hole-face '((((class grayscale) (background light)) :background "lightgrey") @@ -107,8 +104,7 @@ which should be removed when making the text into a hole." :background "mediumblue" :foreground "white") (((class color) (background light)) :background "lightsteelblue" :foreground "black")) - "Font Lock face used to highlight the active hole." - :group 'holes) + "Font Lock face used to highlight the active hole.") ;;; ;;; Keymaps @@ -180,7 +176,7 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).") (defun holes-copy-active-region () "Copy and retuurn the active region." - (assert mark-active nil "the region is not active now.") + (cl-assert mark-active nil "the region is not active now.") (copy-region-as-kill (region-beginning) (region-end)) (car kill-ring)) @@ -190,19 +186,19 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).") (defun holes-hole-start-position (hole) "Return start position of HOLE." - (assert (holes-is-hole-p hole) t + (cl-assert (holes-is-hole-p hole) t "holes-hole-start-position: %s is not a hole") (span-start hole)) (defun holes-hole-end-position (hole) "Return end position of HOLE." - (assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole") + (cl-assert (holes-is-hole-p hole) t "holes-hole-end-position: %s is not a hole") (span-end hole)) (defun holes-hole-buffer (hole) "Return the buffer of HOLE." "Internal." - (assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole") + (cl-assert (holes-is-hole-p hole) t "holes-hole-buffer: %s is not a hole") (span-buffer hole)) (defun holes-hole-at (&optional pos) @@ -221,7 +217,7 @@ active-hole-marker variable)." "Return the position of the start of the active hole. See `active-hole-buffer' to get its buffer. Returns an error if active hole doesn't exist (the marker is set to nothing)." - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "holes-active-hole-start-position: no active hole") (holes-hole-start-position holes-active-hole)) @@ -229,7 +225,7 @@ active hole doesn't exist (the marker is set to nothing)." "Return the position of the start of the active hole. See `active-hole-buffer' to get its buffer. Returns an error if active hole doesn't exist (the marker is set to nothing)." - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "holes-active-hole-end-position: no active hole") (holes-hole-end-position holes-active-hole)) @@ -238,7 +234,7 @@ active hole doesn't exist (the marker is set to nothing)." "Return the buffer containing the active hole. Raise an error if the active hole is not set. Don't care if the active hole is empty." - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "holes-active-hole-buffer: no active hole") (holes-hole-buffer holes-active-hole)) @@ -246,7 +242,7 @@ active hole is empty." "Set point to active hole. Raises an error if active-hole is not set." (interactive) - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "holes-goto-active-hole: no active hole") (goto-char (holes-active-hole-start-position))) @@ -255,7 +251,7 @@ Raises an error if active-hole is not set." "Highlight a HOLE with the `active-hole-face'. DON'T USE this as it would break synchronization (non active hole highlighted)." - (assert (holes-is-hole-p hole) t + (cl-assert (holes-is-hole-p hole) t "holes-highlight-hole-as-active: %s is not a hole") (set-span-face hole 'active-hole-face)) @@ -263,7 +259,7 @@ highlighted)." "Highlight a HOLE with the not active face. DON'T USE this as it would break synchronization (active hole non highlighted)." - (assert (holes-is-hole-p hole) t + (cl-assert (holes-is-hole-p hole) t "holes-highlight-hole: %s is not a hole") (set-span-face hole 'inactive-hole-face)) @@ -283,7 +279,7 @@ the active hole is already disable." (defun holes-set-active-hole (hole) "Set active hole to HOLE. Error if HOLE is not a hole." - (assert (holes-is-hole-p hole) t + (cl-assert (holes-is-hole-p hole) t "holes-set-active-hole: %s is not a hole") (if (holes-active-hole-exist-p) (holes-highlight-hole holes-active-hole)) @@ -328,7 +324,7 @@ the span." (defun holes-clear-hole (hole) "Clear the HOLE." - (assert (holes-is-hole-p hole) t + (cl-assert (holes-is-hole-p hole) t "holes-clear-hole: %s is not a hole") (if (and (holes-active-hole-exist-p) (eq holes-active-hole hole)) @@ -363,11 +359,11 @@ Operate betwenn START and END if non nil." Or after the hole at pos if there is one (default pos=point). If no hole found, return nil." (holes-map-holes - (lambda (h x) (and (holes-is-hole-p h) h)) buffer pos)) + (lambda (h _) (and (holes-is-hole-p h) h)) buffer pos)) (defun holes-next-after-active-hole () "Internal." - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "next-active-hole: no active hole") (holes-next (holes-active-hole-end-position) (holes-active-hole-buffer))) @@ -441,7 +437,7 @@ goal(FIXME?). Use `replace-active-hole' instead." Like `holes-replace-active-hole', but then sets the active hole to the following hole if it exists." (interactive) - (assert (holes-active-hole-exist-p) t + (cl-assert (holes-active-hole-exist-p) t "holes-replace-update-active-hole: no active hole") (if (holes-active-hole-exist-p) (let ((nxthole (holes-next-after-active-hole))) @@ -560,9 +556,9 @@ Sets `holes-active-hole' to the next hole if it exists." "Move the point to current active hole (if any and if in current buffer). Destroy it and makes the next hole active if any." (interactive) - (assert (holes-active-hole-exist-p) nil "no active hole") - (assert (eq (current-buffer) (holes-active-hole-buffer)) nil - "active hole not in this buffer") + (cl-assert (holes-active-hole-exist-p) nil "no active hole") + (cl-assert (eq (current-buffer) (holes-active-hole-buffer)) nil + "active hole not in this buffer") (holes-goto-active-hole) (holes-delete-update-active-hole)) @@ -593,7 +589,7 @@ The LIMIT argument bounds the search; it is a buffer position. (let ((n 0)) (save-excursion (while (re-search-backward holes-empty-hole-regexp limit t) - (incf n) + (cl-incf n) (if (not (match-end 1)) (holes-make-hole (match-beginning 0) (match-end 0)) (holes-make-hole (match-beginning 1) (match-end 1)) @@ -625,12 +621,12 @@ If NOINDENT is non-nil, skip the indenting step. If ALWAYSJUMP is non-nil, jump to the first hole even if more than one." (unless noindent (save-excursion (indent-region pos (point) nil))) (let ((n (holes-replace-string-by-holes-backward pos))) - (case n - (0 nil) ; no hole, stay here. - (1 + (pcase n + (`0 nil) ; no hole, stay here. + (`1 (goto-char pos) (holes-set-point-next-hole-destroy)) ; if only one hole, go to it. - (t + (_ (goto-char pos) (when alwaysjump (holes-set-point-next-hole-destroy)) (unless (active-minibuffer-window) ; otherwise minibuffer gets hidden @@ -727,10 +723,9 @@ it mean anyway?) o Cutting or pasting a hole will not produce new holes, and undoing on holes cannot make holes re-appear." nil " Holes" holes-mode-map - :group 'holes (if holes-mode - (add-hook 'skeleton-end-hook 'holes-skeleton-end-hook nil t) - (remove-hook 'skeleton-end-hook 'holes-skeleton-end-hook t) + (add-hook 'skeleton-end-hook #'holes-skeleton-end-hook nil t) + (remove-hook 'skeleton-end-hook #'holes-skeleton-end-hook t) (holes-clear-all-buffer-holes))) ;;;###autoload diff --git a/lib/pg-dev.el b/lib/pg-dev.el index 8e82a753..78d79862 100644 --- a/lib/pg-dev.el +++ b/lib/pg-dev.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,9 +24,6 @@ (require 'whitespace) (eval-when-compile - (require 'cl)) - -(eval-when-compile (require 'proof-site)) (with-no-warnings diff --git a/lib/proof-compat.el b/lib/proof-compat.el index abbdb465..95c533e5 100644 --- a/lib/proof-compat.el +++ b/lib/proof-compat.el @@ -1,9 +1,9 @@ -;;; proof-compat.el --- Operating system and Emacs version compatibility +;;; proof-compat.el --- Operating system and Emacs version compatibility -*- 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 @@ -28,28 +28,7 @@ ;;; Code: -(require 'easymenu) -(require 'cl) - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; Architecture flags -;;; - -;; can use eval-and-compile to allow optimisation, but that would -;; require recompilation for Windows -(defvar proof-running-on-win32 (memq system-type '(win32 windows-nt cygwin)) - "Non-nil if Proof General is running on a windows variant system.") - - -;; Workaround a small bug in Carbon Emacs Winter 2008 (at least) -;; Menu presses query this variable, but it's not bound unless -;; mode engaged. Not noticeable in normal use, but it is as soon -;; as debug-on-error is engaged. -(with-no-warnings - (if (and (boundp 'carbon-emacs-package-version) - (not (boundp 'mac-key-mode))) - (setq mac-key-mode nil))) +(require 'cl-lib) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;;; @@ -64,8 +43,8 @@ Done by removing all properties mentioned by custom library. The symbol itself is left defined, in case it has been changed in the current Emacs session." - (mapc (lambda (prop) (remprop symbol prop)) - '(default + (dolist (prop + '(default standard-value force-value variable-comment @@ -83,49 +62,8 @@ in the current Emacs session." custom-version saved-value theme-value - theme-face))) - - -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;;; -;;; GNU Emacs compatibility with XEmacs -;;; - -(unless (fboundp 'save-selected-frame) -(defmacro save-selected-frame (&rest body) - "Execute forms in BODY, then restore the selected frame. -The value returned is the value of the last form in BODY." - (let ((old-frame (gensym "ssf"))) - `(let ((,old-frame (selected-frame))) - (unwind-protect - (progn ,@body) - (select-frame ,old-frame)))))) - -;; These functions are used in the intricate logic around -;; shrink-to-fit. - -;; window-leftmost-p, window-rightmost-p: my implementations -(or (fboundp 'window-leftmost-p) - (defun window-leftmost-p (window) - (zerop (car (window-edges window))))) - -(or (fboundp 'window-rightmost-p) - (defun window-rightmost-p (window) - (>= (nth 2 (window-edges window)) - (frame-width (window-frame window))))) - -(or (fboundp 'window-bottom-p) - (defun window-bottom-p (window) - (>= (nth 3 (window-edges window)) - (frame-height (window-frame window))))) - -;; find-coding-system emulation for GNU Emacs -(unless (fboundp 'find-coding-system) - (defun find-coding-system (name) - "Retrieve the coding system of the given name, or nil if non-such." - (condition-case nil - (check-coding-system name) - (error nil)))) + theme-face)) + (cl-remprop symbol prop))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; @@ -137,9 +75,9 @@ The value returned is the value of the last form in BODY." ;; makes every suffix be added as a completion! (eval-after-load "completion" -'(defun completion-before-command () - (if (and (symbolp this-command) (get this-command 'completion-function)) - (funcall (get this-command 'completion-function))))) + '(defun completion-before-command () + (if (and (symbolp this-command) (get this-command 'completion-function)) + (funcall (get this-command 'completion-function))))) (provide 'proof-compat) ;;; proof-compat.el ends here diff --git a/lib/span.el b/lib/span.el index e7e3d68b..4bb7507e 100644 --- a/lib/span.el +++ b/lib/span.el @@ -1,9 +1,9 @@ -;;; span.el --- Datatype of "spans" for Proof General +;;; span.el --- Datatype of "spans" for Proof General -*- 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 @@ -24,8 +24,6 @@ ;;; Code: -(eval-when-compile (require 'cl)) ;For lexical-let. - (defalias 'span-start 'overlay-start) (defalias 'span-end 'overlay-end) (defalias 'span-set-property 'overlay-put) @@ -42,10 +40,9 @@ "Check if an overlay OL belongs to PG." (overlay-get ol 'pg-span)) -(defun span-read-only-hook (overlay after start end &optional len) +(defun span-read-only-hook (&rest _) (unless inhibit-read-only - (error "Region is read-only"))) -(add-to-list 'debug-ignored-errors "Region is read-only") + (user-error "Region is read-only"))) (defun span-read-only (span) "Set SPAN to be read only." @@ -61,12 +58,11 @@ (defun span-write-warning (span fun) "Give a warning message when SPAN is changed, unless `inhibit-read-only' is non-nil." - (lexical-let ((fun fun)) - (let ((funs (list (lambda (span afterp beg end &rest args) - (if (and (not afterp) (not inhibit-read-only)) - (funcall fun beg end)))))) - (span-set-property span 'modification-hooks funs) - (span-set-property span 'insert-in-front-hooks funs)))) + (let ((funs (list (lambda (_span afterp beg end &rest _) + (if (and (not afterp) (not inhibit-read-only)) + (funcall fun beg end)))))) + (span-set-property span 'modification-hooks funs) + (span-set-property span 'insert-in-front-hooks funs))) ;; We use end first because proof-locked-queue is often changed, and ;; its starting point is always 1 @@ -155,13 +151,13 @@ A span is before PT if it begins before the character before PT." (overlay-buffer span) (buffer-live-p (overlay-buffer span)))) -(defun span-raise (span) - "Set priority of SPAN to make it appear above other spans." - ;; FIXME: Emacs already uses a "shorter goes above" which takes care of - ;; preventing a span from seeing another. So don't play with - ;; priorities, please! - ;; (span-set-property span 'priority 100) - ) +;; (defun span-raise (_span) +;; "Set priority of SPAN to make it appear above other spans." +;; ;; FIXME: Emacs already uses a "shorter goes above" which takes care of +;; ;; preventing a span from seeing another. So don't play with +;; ;; priorities, please! +;; ;; (span-set-property span 'priority 100) +;; ) (defun span-string (span) (with-current-buffer (overlay-buffer span) @@ -180,7 +176,7 @@ A span is before PT if it begins before the character before PT." (overlays-at (posn-point (event-start event))) (or prop 'span)))) -(defun fold-spans (f &optional buffer from to maparg ignored-flags prop val) +(defun fold-spans (f &optional buffer from to maparg _ignored-flags prop val) (with-current-buffer (or buffer (current-buffer)) (let ((ols (overlays-in (or from (point-min)) (or to (point-max)))) res) @@ -238,7 +234,7 @@ The span will remove itself after a timeout of 2 seconds." (add-timeout 2 'delete-overlay ol) ol)) -(defun span-delete-self-modification-hook (span &rest args) +(defun span-delete-self-modification-hook (span &rest _) "Hook for overlay modification-hooks, which deletes SPAN." (if (span-live-p span) (span-delete span))) @@ -252,7 +248,7 @@ Return the span." (overlay-put ol (car props) (cadr props)) (setq props (cddr props))) (span-set-property ol 'modification-hooks - (list 'span-delete-self-modification-hook)) + (list #'span-delete-self-modification-hook)) ol)) diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el index e39ee51a..2d6a3cf4 100644 --- a/lib/texi-docstring-magic.el +++ b/lib/texi-docstring-magic.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 @@ -92,9 +92,6 @@ ;;; Code: -(eval-when-compile - (require 'cl)) - (defun texi-docstring-magic-find-face (face) "Return non-nil if FACE is a face name; nil otherwise. A face name can be a string or a symbol. diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index 4d1d0d35..41f478d1 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -46,7 +46,7 @@ ;;; Code: -(require 'cl) +(require 'cl-lib) (require 'quail) (eval-when-compile @@ -429,12 +429,12 @@ This function also initialises the important tables for the mode." ;; hairy logic based on Coq-style vs Isabelle-style configs (if (string= "" (format unicode-tokens-token-format "")) ;; no special token format, parse separate words/symbols - (let* ((tokextra (remove* "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match)) - (toksymbwrd (set-difference toks tokextra)) + (let* ((tokextra (cl-remove "^\\(?:\\sw\\|\\s_\\)+$" toks :test 'string-match)) + (toksymbwrd (cl-set-difference toks tokextra)) ;; indentifier that are not pure words - (toksymb (remove* "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match)) + (toksymb (cl-remove "^\\(?:\\sw\\)+$" toksymbwrd :test 'string-match)) ;; pure words - (tokwrd (set-difference toksymbwrd toksymb)) + (tokwrd (cl-set-difference toksymbwrd toksymb)) (idorop (concat "\\(\\_<" (regexp-opt toksymb) @@ -461,9 +461,9 @@ This function also initialises the important tables for the mode." The check is with `char-displayable-p'." (cond ((stringp comp) - (reduce (lambda (x y) (and x (char-displayable-p y))) - comp - :initial-value t)) + (cl-reduce (lambda (x y) (and x (char-displayable-p y))) + comp + :initial-value t)) ((characterp comp) (char-displayable-p comp)) (comp ;; assume any other non-null is OK @@ -518,7 +518,7 @@ The face property is set to the :family and :slant attriubutes taken from (car props) (cadr props)) (setq props (cddr props))))) (unless (or unicode-tokens-show-symbols - (intersection unicode-tokens-fonts propsyms)) + (cl-intersection unicode-tokens-fonts propsyms)) (font-lock-append-text-property start end 'face ;; just use family and slant to enhance merging with other faces @@ -680,7 +680,7 @@ Calculated from `unicode-tokens-token-name-alist' and `unicode-tokens-shortcut-alist'." (let ((unicode-tokens-quail-define-rules (list 'quail-define-rules))) - (let ((ulist (copy-list unicode-tokens-shortcut-alist)) + (let ((ulist (copy-sequence unicode-tokens-shortcut-alist)) ustring shortcut) (setq ulist (sort ulist 'unicode-tokens-map-ordering)) (while ulist @@ -714,7 +714,7 @@ Available annotations chosen from `unicode-tokens-control-regions'." "Annotate region with: " unicode-tokens-control-regions nil 'requirematch)))) - (assert (assoc name unicode-tokens-control-regions)) + (cl-assert (assoc name unicode-tokens-control-regions)) (let* ((entry (assoc name unicode-tokens-control-regions)) (beg (region-beginning)) (end (region-end)) @@ -736,7 +736,7 @@ Available annotations chosen from `unicode-tokens-control-regions'." "Insert control symbol: " unicode-tokens-control-characters nil 'requirematch))) - (assert (assoc name unicode-tokens-control-characters)) + (cl-assert (assoc name unicode-tokens-control-characters)) (insert (format unicode-tokens-control-char-format (cadr (assoc name unicode-tokens-control-characters))))) @@ -833,7 +833,8 @@ but multiple characters in the underlying buffer." (error "Cannot find token before point")) (when token (let* ((tokennumber - (search (list token) unicode-tokens-token-list :test 'equal)) + (cl-search (list token) unicode-tokens-token-list + :test #'equal)) (numtoks (hash-table-count unicode-tokens-hash-table)) (newtok @@ -943,7 +944,7 @@ Starts from point." 'face 'header-line)) (insert " ")) - (incf count) + (cl-incf count) (if (null toks) (insert " ") (insert-text-button diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el index f5462ba6..cf69a731 100644 --- a/obsolete/plastic/plastic.el +++ b/obsolete/plastic/plastic.el @@ -1,5 +1,7 @@ ;; plastic.el - Major mode for Plastic proof assistant ;; +;; Portions © Copyright 2018 Free Software Foundation, Inc. +;; ;; Author: Paul Callaghan <P.C.Callaghan@durham.ac.uk> ;; ;; $Id$ @@ -11,12 +13,12 @@ (require 'proof) +(require 'cl-lib) ;cl-member-if (eval-when-compile - (require 'cl) (require 'span) (require 'proof-syntax) - (require 'outline) - (defvar plastic-keymap nil)) + (require 'outline)) +(defvar plastic-keymap) ;FIXME: Not defined anywhere! (require 'plastic-syntax) @@ -227,7 +229,7 @@ Given is the first SPAN which needs to be undone." (setq i 0) (while (< i (length string)) (if (string-equal (substring string i (+ i tl)) proof-terminal-string) - (incf ct)) + (cl-incf ct)) (setq i (+ 1 i))))) (setq span (next-span span 'type))) (list (concat plastic-lit-string @@ -262,9 +264,9 @@ Given is the first SPAN which needs to be undone." ; (list (concat "Can't Undo imports yet\n" ; "You have to exit Plastic for this\n") ; ["ok, I'll do this" (lambda () t) t])) - (return) + (cl-return) ;FIXME: No enclosing block?! ) ;; warn the user that undo of imports not yet working. - (t (incf spans)) + (t (cl-incf spans)) ) (setq span (next-span span 'type)) @@ -451,7 +453,7 @@ Value for `proof-shell-compute-new-files-list', which see. For Plastic, we assume that module identifiers coincide with file names." (let ((module (match-string 1))) - (cdr (member-if + (cdr (cl-member-if (lambda (filename) (plastic-equal-module-filename module filename)) proof-included-files-list)))) @@ -539,33 +541,33 @@ For Plastic, we assume that module identifiers coincide with file names." (l (length string)) (eat-rest (lambda () (aset string i ?\ ) ;; kill the \n or "-" at least - (incf i) + (cl-incf i) (while (and (< i l) (/= (aref string i) ?\n)) (aset string i ?\ ) - (incf i) ))) + (cl-incf i) ))) (keep-rest (lambda () (loop for x in (string-to-list plastic-lit-string) - do (aset string i ?\ ) (incf i)) + do (aset string i ?\ ) (cl-incf i)) (while (and (< i l) (/= (aref string i) ?\n) (/= (aref string i) ?-)) - (incf i) )))) + (cl-incf i) )))) (while (< i l) (cond ((eq 0 (string-match "--" (substring string i))) (funcall eat-rest)) ; comment. ((eq 0 (string-match "\n\n" (substring string i))) (aset string i ?\ ) - (incf i)) ; kill repeat \n + (cl-incf i)) ; kill repeat \n ((= (aref string i) ?\n) ; start of new line - (aset string i ?\ ) (incf i) ; remove \n + (aset string i ?\ ) (cl-incf i) ; remove \n (if (eq 0 (string-match plastic-lit-string (substring string i))) (funcall keep-rest) ; code line. (funcall eat-rest) ; non-code line )) (t - (incf i)))) ; else include. + (cl-incf i)))) ; else include. (setq string (replace-regexp-in-string " +" " " string)) (setq string (replace-regexp-in-string "^ +" "" string)) (if (string-match "^\\s-*$" string) @@ -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 @@ -42,25 +42,10 @@ ;;; Code: ;;;###autoload -(eval-and-compile - (defvar pg-init--script-full-path - (or (and load-in-progress load-file-name) - (bound-and-true-p byte-compile-current-file) - (buffer-file-name))) - (defvar pg-init--pg-root - (file-name-directory pg-init--script-full-path))) - -;;;###autoload -(unless (bound-and-true-p byte-compile-current-file) - ;; This require breaks compilation, so it must only run when loading the package. - (require 'proof-site (expand-file-name "generic/proof-site" pg-init--pg-root))) - -(eval-when-compile - (let ((byte-compile-directories - '("generic" "lib" - "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"))) - (dolist (dir byte-compile-directories) - (add-to-list 'load-path (expand-file-name dir pg-init--pg-root))))) +(if t (require 'proof-site + (expand-file-name "generic/proof-site" + (file-name-directory + (or load-file-name buffer-file-name))))) (provide 'pg-init) ;;; pg-init.el ends here |