> Pushed as well. Thanks!
[ Tant que je gagne, je joue! ]
Here's another,
Stefan
>From 5549c4751e7e73382d2bd088322a483df90f51c9 Mon Sep 17 00:00:00 2001
From: Stefan Monnier <monn...@iro.umontreal.ca>
Date: Thu, 13 Dec 2018 22:57:15 -0500
Subject: [PATCH] Fix remaining uses of CL; Make files more declarative
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit
Emacs occasionally loads Elisp files just to get more info (e.g. for C-h f),
so loading a file should "no effect". Fix the most obvious such effects:
the splash screen and the autotests by moving those effects into a function.
* coq/coq-autotest.el: Make it declarative. Use lexical-binding.
(coq-autotest): New function holding the code that used to be at top-level.
* generic/proof.el: Use lexical-binding.
Don't call proof-splash-message just because we're being loaded.
* generic/proof-script.el: Use lexical-scoping; fix all warnings.
(pg-show-all-portions): Simplify the code with a closure.
(proof-activate-scripting): Declare activated-interactively as dyn-scoped.
(proof--splash-done): New var.
(proof-mode): Call proof-splash-message upon first use.
* generic/proof-splash.el (proof-splash-message): Don't check
byte-compile-current-file now that we're only called when the mode
is activated.
* acl2/acl2.el (auto-mode-alist): Use `add-to-list` and \'.
* coq/coq-db.el (coq-build-menu-from-db-internal): Avoid silly O(N²).
* coq/coq-seq-compile.el:
* coq/coq-par-test.el:
* coq/coq-par-compile.el: Fix leftover uses of CL's `assert`.
* generic/proof-utils.el:
* generic/pg-movie.el:
* etc/testsuite/pg-test.el:
* coq/coq-syntax.el: Fix leftover uses of CL's `incf`.
* generic/pg-autotest.el: Fix leftover uses of CL's `decf`.
* obsolete/plastic/plastic.el (plastic-preprocessing): Fix leftover use
of CL's `loop`.
* generic/pg-user.el (proof-add-completions): Do nothing if no
proof-assistant is set yet (i.e. during byte-compilation).
(byte-compile-current-file): No need to test this any more.
* generic/proof-syntax.el (proof-regexp-alt-list): Use mapconcat.
Remove unnecessary "\\(?:...\\)".
(proof-regexp-alt): Redefine in terms of proof-regexp-alt-list.
---
acl2/acl2.el | 9 ++---
coq/coq-autotest.el | 6 ++-
coq/coq-db.el | 16 ++++----
coq/coq-par-compile.el | 34 ++++++++--------
coq/coq-par-test.el | 35 +++++++++--------
coq/coq-seq-compile.el | 5 ++-
coq/coq-syntax.el | 17 ++++----
etc/testsuite/pg-test.el | 8 ++--
generic/pg-autotest.el | 9 +++--
generic/pg-movie.el | 5 ++-
generic/pg-user.el | 16 ++++----
generic/proof-script.el | 96 +++++++++++++++++++++++----------------------
generic/proof-splash.el | 4 +-
generic/proof-syntax.el | 14 +++----
generic/proof-useropts.el | 4 +-
generic/proof-utils.el | 6 +--
generic/proof.el | 5 +--
obsolete/plastic/plastic.el | 4 +-
18 files changed, 147 insertions(+), 146 deletions(-)
diff --git a/acl2/acl2.el b/acl2/acl2.el
index cf9f521c..db3120ed 100644
--- a/acl2/acl2.el
+++ b/acl2/acl2.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,10 +24,9 @@
(require 'proof-easy-config) ; easy configure mechanism
(require 'proof-syntax) ; functions for making regexps
-(setq auto-mode-alist ; ACL2 uses two file extensions
- (cons ; Only grab .lisp extension after
- (cons "\\.lisp$" 'acl2-mode) ; an acl2 file has been loaded
- auto-mode-alist))
+(add-to-list 'auto-mode-alist ; ACL2 uses two file extensions
+ ; Only grab .lisp extension after
+ (cons "\\.lisp\\'" 'acl2-mode)) ; an acl2 file has been loaded
(proof-easy-config 'acl2 "ACL2"
proof-assistant-home-page "http://www.cs.utexas.edu/users/moore/acl2";
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el
index 8be4bed9..5ca66706 100644
--- a/coq/coq-autotest.el
+++ b/coq/coq-autotest.el
@@ -1,4 +1,4 @@
-;;; coq-autotest.el --- tests of Coq Proof General (in progress).
+;;; coq-autotest.el --- tests of Coq Proof General (in progress) -*- lexical-binding:t -*-
;; This file is part of Proof General.
@@ -21,7 +21,9 @@
(require 'proof-site)
(defvar coq-compile-before-require)
-(unless (bound-and-true-p byte-compile-current-file)
+;;;###autoload
+(defun coq-autotest ()
+ (interactive)
(pg-autotest start 'debug)
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 36812c4c..7e59bffb 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -25,7 +25,7 @@
(eval-when-compile (require 'cl-lib)) ;decf
-(require 'proof-config) ; for proof-face-specs, a macro
+(require 'proof-config)
(require 'proof-syntax) ; for proof-ids-to-regexp
(require 'holes)
@@ -187,7 +187,7 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See
(let ((l db) (res ()) (size lgth)
(keybind-abbrev (substitute-command-keys " \\[expand-abbrev]")))
(while (and l (> size 0))
- (let* ((hd (car l))
+ (let* ((hd (pop l))
(menu (nth 0 hd)) ; e1 = menu entry
(abbrev (nth 1 hd)) ; e2 = abbreviation
(complt (nth 2 hd)) ; e3 = completion
@@ -209,10 +209,9 @@ Used by `coq-build-menu-from-db', which you should probably use instead. See
;;insertion function if present otherwise insert completion
(if insertfn insertfn `(holes-insert-and-expand ,complt))
t)))
- (setq res (nconc res (list menu-entry)))));; append *in place*
- (setq l (cdr l))
+ (push menu-entry res)))
(cl-decf size)))
- res))
+ (nreverse res)))
(defun coq-build-title-menu (db size)
@@ -289,10 +288,9 @@ See `coq-syntax-db' for DB structure."
;;A new face for tactics which fail when they don't kill the current goal
(defface coq-solve-tactics-face
- (proof-face-specs
- (:foreground "red") ; pour les fonds clairs
- (:foreground "red1") ; pour les fonds foncés
- ()) ; pour le noir et blanc
+ `((((background light)) :foreground "red")
+ (((background dark)) :foreground "red1")
+ ()) ; pour le noir et blanc
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index c6822dc5..ac2e82bf 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -35,7 +35,7 @@
;;; Code:
(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
-
+(eval-when-compile (require 'cl-lib))
(require 'coq-compile-common)
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -712,7 +712,7 @@ function returns () if MODULE-ID comes from the standard library."
;; error-message)))
;; (coq-seq-display-compile-response-buffer)
(error error-message)))
- (assert (<= (length result) 1)
+ (cl-assert (<= (length result) 1)
nil "Internal error in coq-seq-map-module-id-to-obj-file")
(car-safe result)))
@@ -949,7 +949,7 @@ errors are reported with an error message."
(defun coq-par-run-vio2vo-queue ()
"Start delayed vio2vo compilation."
- (assert (not coq--last-compilation-job)
+ (cl-assert (not coq--last-compilation-job)
nil "normal compilation and vio2vo in parallel 3")
(setq coq--compile-vio2vo-in-progress t)
(setq coq--compile-vio2vo-delay-timer nil)
@@ -1011,7 +1011,7 @@ somewhere after the last require command."
(defun coq-par-add-queue-dependency (dependee dependant)
"Add queue dependency from child job DEPENDEE to parent job DEPENDANT."
- (assert (and (not (get dependant 'queue-dependant-waiting))
+ (cl-assert (and (not (get dependant 'queue-dependant-waiting))
(not (get dependee 'queue-dependant)))
nil "queue dependency cannot be added")
(put dependant 'queue-dependant-waiting t)
@@ -1202,13 +1202,13 @@ when they transition from 'waiting-queue to 'ready:
This function can safely be called for non-top-level jobs. This
function must not be called for failed jobs."
- (assert (not (get job 'failed))
+ (cl-assert (not (get job 'failed))
nil "coq-par-retire-top-level-job precondition failed")
(let ((span (get job 'require-span))
(items (get job 'queueitems)))
(when (and span coq-lock-ancestors)
(dolist (anc-job (get job 'ancestors))
- (assert (not (eq (get anc-job 'lock-state) 'unlocked))
+ (cl-assert (not (eq (get anc-job 'lock-state) 'unlocked))
nil "bad ancestor lock state")
(when (eq (get anc-job 'lock-state) 'locked)
(put anc-job 'lock-state 'asserted)
@@ -1290,7 +1290,7 @@ case, the following actions are taken:
(let ((dependant (get job 'queue-dependant)))
(if dependant
(progn
- (assert (not (eq coq--last-compilation-job job))
+ (cl-assert (not (eq coq--last-compilation-job job))
nil "coq--last-compilation-job invariant error")
(put dependant 'queue-dependant-waiting nil)
(when coq--debug-auto-compilation
@@ -1309,7 +1309,7 @@ case, the following actions are taken:
(proof-script-clear-queue-spans-on-error nil))
(proof-release-lock)
(when (eq coq-compile-quick 'quick-and-vio2vo)
- (assert (not coq--compile-vio2vo-delay-timer)
+ (cl-assert (not coq--compile-vio2vo-delay-timer)
nil "vio2vo timer set before last compilation job")
(setq coq--compile-vio2vo-delay-timer
(run-at-time coq-compile-vio2vo-delay nil
@@ -1362,7 +1362,7 @@ if it reaches 0, the next transition is triggered for DEPENDANT.
For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
'clone jobs this 'waiting-dep -> 'waiting-queue."
;(message "%s: CPDCD with time %s" (get dependant 'name) dependee-time)
- (assert (eq (get dependant 'state) 'waiting-dep)
+ (cl-assert (eq (get dependant 'state) 'waiting-dep)
nil "wrong state of parent dependant job")
(when (coq-par-time-less (get dependant 'youngest-coqc-dependency)
dependee-time)
@@ -1371,7 +1371,7 @@ For 'file jobs this is 'waiting-dep -> 'enqueued-coqc and for
(append dependee-ancestors (get dependant 'ancestors)))
(put dependant 'coqc-dependency-count
(1- (get dependant 'coqc-dependency-count)))
- (assert (<= 0 (get dependant 'coqc-dependency-count))
+ (cl-assert (<= 0 (get dependant 'coqc-dependency-count))
nil "dependency count below zero")
(when coq--debug-auto-compilation
(message "%s: coqc dependency count down to %d"
@@ -1439,7 +1439,7 @@ This function makes the following actions.
"maybe kickoff queue")
(get job 'name)
(if dependant-alive "some" "no")))
- (assert (or (not (get job 'failed)) (not dependant-alive))
+ (cl-assert (or (not (get job 'failed)) (not dependant-alive))
nil "failed job with non-failing dependant")
(when (or (and (not dependant-alive)
(not (get job 'require-span))
@@ -1512,7 +1512,7 @@ coqdep or coqc are started for it."
(get job 'required-obj-file))))
((eq job-state 'ready)
(coq-par-start-vio2vo job))
- (t (assert nil nil "coq-par-start-task with invalid job")))))
+ (t (cl-assert nil nil "coq-par-start-task with invalid job")))))
(defun coq-par-start-jobs-until-full ()
"Start background jobs until the limit is reached."
@@ -1622,7 +1622,7 @@ Return t if job has a direct or indirect dependant that has not
failed yet and that is in a state before 'waiting-queue. Also,
return t if JOB has a dependant that is a top-level job which has
not yet failed."
- (assert (not (eq (get job 'lock-state) 'asserted))
+ (cl-assert (not (eq (get job 'lock-state) 'asserted))
nil "coq-par-ongoing-compilation precondition failed")
(cond
((get job 'failed)
@@ -1653,7 +1653,7 @@ not yet failed."
(setq res (coq-par-ongoing-compilation dep)))
res))
(t
- (assert nil nil
+ (cl-assert nil nil
"impossible ancestor state %s on job %s"
(get job 'state) (get job 'name)))))
@@ -1680,7 +1680,7 @@ Mark JOB with 'queue-failed, and, if JOB is in state
appropriate."
(unless (or (get job 'failed) (get job 'queue-failed))
(put job 'queue-failed t)
- (assert (not (eq (get job 'state) 'ready))
+ (cl-assert (not (eq (get job 'state) 'ready))
nil "coq-par-mark-queue-failing impossible state")
(when coq--debug-auto-compilation
(message "%s: mark as queue-failed, %s"
@@ -1893,7 +1893,7 @@ there is no last compilation job."
;; add the asserted items to the last compilation job
(if coq--last-compilation-job
(progn
- (assert (not (coq-par-job-is-ready coq--last-compilation-job))
+ (cl-assert (not (coq-par-job-is-ready coq--last-compilation-job))
nil "last compilation job from previous compilation ready")
(put coq--last-compilation-job 'queueitems
(nconc (get coq--last-compilation-job 'queueitems)
@@ -1979,7 +1979,7 @@ the maximal number of background compilation jobs is started."
(cancel-timer coq--compile-vio2vo-delay-timer)
(setq coq--compile-vio2vo-delay-timer nil))
(when coq--compile-vio2vo-in-progress
- (assert (not coq--last-compilation-job)
+ (cl-assert (not coq--last-compilation-job)
nil "normal compilation and vio2vo in parallel 2")
;; there are only vio2vo background processes
(coq-par-kill-all-processes)
diff --git a/coq/coq-par-test.el b/coq/coq-par-test.el
index ebc5ecd7..f2e3f01d 100644
--- a/coq/coq-par-test.el
+++ b/coq/coq-par-test.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
@@ -31,6 +31,7 @@
;;; Code:
(require 'coq-par-compile)
+(eval-when-compile (require 'cl-lib))
(defconst coq--par-job-needs-compilation-tests
;; for documentation see the doc string following the init value
@@ -753,7 +754,7 @@ relative ages.")
(lambda (test)
(let ((test-id (format "%s" (car test))))
;; a test is a list of 4 elements and the first element is a list itself
- (assert
+ (cl-assert
(and
(eq (length test) 4)
(listp (car test)))
@@ -761,22 +762,22 @@ relative ages.")
(mapc
(lambda (variant)
;; a variant is a list of 4 elements
- (assert (eq (length variant) 4) nil (concat test-id " 2"))
+ (cl-assert (eq (length variant) 4) nil (concat test-id " 2"))
(let ((files (coq-par-test-flatten-files (car test)))
(quick-mode (car variant))
(compilation-result (nth 1 variant))
(delete-result (nth 2 variant))
(req-obj-result (nth 3 variant)))
;; the delete field, when set, must be a member of the files list
- (assert (or (not delete-result)
+ (cl-assert (or (not delete-result)
(member delete-result files))
nil (concat test-id " 3"))
;; 8.4 compatibility check
(when (and (or (eq quick-mode 'no-quick) (eq quick-mode 'ensure-vo))
(not (member 'vio files)))
- (assert (not delete-result)
+ (cl-assert (not delete-result)
nil (concat test-id " 4"))
- (assert (eq compilation-result
+ (cl-assert (eq compilation-result
(not (eq (car (last (car test))) 'vo)))
nil (concat test-id " 5")))))
(cdr test))))
@@ -789,7 +790,7 @@ relative ages.")
((eq sym 'dep) "dep.vo")
((eq sym 'vo) "a.vo")
((eq sym 'vio) "a.vio")
- (t (assert nil)))))
+ (t (cl-assert nil)))))
(concat dir "/" file)))
(defun test-coq-par-one-test (counter dir file-descr variant dep-just-compiled)
@@ -832,7 +833,7 @@ test the result and side effects wth `assert'."
;; different-counter (current-time))
(setq different-not-ok nil)
(setq different-counter (1- different-counter))
- (assert (> different-counter 0)
+ (cl-assert (> different-counter 0)
nil "create files with different time stamps failed")
(dolist (same-descr file-descr)
(when (symbolp same-descr)
@@ -845,7 +846,7 @@ test the result and side effects wth `assert'."
(setq same-not-ok t)
(while same-not-ok
(setq same-counter (1- same-counter))
- (assert (> same-counter 0)
+ (cl-assert (> same-counter 0)
nil "create files with same time stamp filed")
(dolist (file file-list)
(with-temp-file file t))
@@ -875,40 +876,40 @@ test the result and side effects wth `assert'."
(put job 'youngest-coqc-dependency 'just-compiled))
(setq result (coq-par-job-needs-compilation job))
;; check result
- (assert (eq result compilation-result)
+ (cl-assert (eq result compilation-result)
nil (concat id " result"))
;; check file deletion
- (assert (or (not delete-result)
+ (cl-assert (or (not delete-result)
(not (file-attributes
(test-coq-par-sym-to-file dir delete-result))))
nil (concat id " delete file"))
;; check no other file is deleted
(dolist (f file-descr-flattened)
(unless (eq f delete-result)
- (assert (file-attributes (test-coq-par-sym-to-file dir f))
+ (cl-assert (file-attributes (test-coq-par-sym-to-file dir f))
nil (format "%s non del file %s: %s"
id f
(test-coq-par-sym-to-file dir f)))))
;; check value of 'required-obj-file property
- (assert (equal (get job 'required-obj-file)
+ (cl-assert (equal (get job 'required-obj-file)
(test-coq-par-sym-to-file dir req-obj-result))
nil (concat id " required-obj-file"))
;; check 'obj-mod-time property
(if obj-mod-result
- (assert
+ (cl-assert
(equal
(get job 'obj-mod-time)
(nth 5 (file-attributes
(test-coq-par-sym-to-file dir obj-mod-result))))
nil (concat id " obj-mod-time non nil"))
- (assert (not (get job 'obj-mod-time))
+ (cl-assert (not (get job 'obj-mod-time))
nil (concat id " obj-mod-time nil")))
;; check 'use-quick property
- (assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
+ (cl-assert (eq (not (not (and compilation-result (eq req-obj-result 'vio))))
(get job 'use-quick))
nil (concat id " use-quick"))
;; check vio2vo-needed property
- (assert (eq
+ (cl-assert (eq
(and (eq quick-mode 'quick-and-vio2vo)
(eq req-obj-result 'vio)
(or (eq delete-result 'vo)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 4889ccaf..3cdcd02a 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -24,6 +24,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
(defvar queueitems) ; dynamic scope in p-s-extend-queue-hook
(require 'coq-compile-common)
@@ -335,8 +336,8 @@ function returns () if MODULE-ID comes from the standard library."
;; error-message)))
;; (coq-display-compile-response-buffer)
(error error-message)))
- (assert (<= (length result) 1)
- "Internal error in coq-seq-map-module-id-to-obj-file")
+ (cl-assert (<= (length result) 1)
+ "Internal error in coq-seq-map-module-id-to-obj-file")
(car-safe result)))
(defun coq-seq-check-module (coq-object-local-hash-symbol span module-id &optional from)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index bb32fc52..e1a9a7e3 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-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
@@ -19,6 +19,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
(require 'proof-syntax)
(require 'proof-utils) ; proof-locate-executable
(require 'coq-db)
@@ -509,12 +510,12 @@ so for the following reasons:
)
;; modules and section are indented like goal starters
-;;; PC TODO: this category is used only for indentation, because
-;;; scripting uses information from coq to decide if a goal is
-;;; started. Since it is impossible for some commands to know
-;;; syntactically if they start something (ex: Instance), the
-;;; right thing to do would be to indent only on "Proof." and forget
-;;; about this category for indentation.
+;; PC TODO: this category is used only for indentation, because
+;; scripting uses information from coq to decide if a goal is
+;; started. Since it is impossible for some commands to know
+;; syntactically if they start something (ex: Instance), the
+;; right thing to do would be to indent only on "Proof." and forget
+;; about this category for indentation.
(defvar coq-goal-starters-db
'(
@@ -991,7 +992,7 @@ so for the following reasons:
Empty matches are counted once."
(let ((nbmatch 0) (str strg))
(while (and (proof-string-match regexp str) (not (string-equal str "")))
- (incf nbmatch)
+ (cl-incf nbmatch)
(if (= (match-end 0) 0) (setq str (substring str 1))
(setq str (substring str (match-end 0)))))
nbmatch))
diff --git a/etc/testsuite/pg-test.el b/etc/testsuite/pg-test.el
index 2e3c2c10..2c064827 100644
--- a/etc/testsuite/pg-test.el
+++ b/etc/testsuite/pg-test.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
@@ -14,6 +14,8 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
+
(defconst pg-test-buffer "** PG test output **")
(defvar pg-test-total-success-count 0)
@@ -68,8 +70,8 @@
(format " %s failed: exprected result %s, got %s\n"
name goodresult result))))
(if errorresult
- (incf pg-test-suite-fail-count)
- (incf pg-test-suite-success-count)
+ (cl-incf pg-test-suite-fail-count)
+ (cl-incf pg-test-suite-success-count)
(setq errorresult (format " %s succeeded.\n" name)))
;; Return string
errorresult))
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index e7cb19a9..7a22c9f7 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-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
@@ -25,6 +25,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
(require 'proof-splash)
(setq proof-splash-enable nil) ; prevent splash when testing
@@ -215,7 +216,7 @@ completely processing the buffer as the last step."
" random jump: processing whole buffer")
(proof-process-buffer)
(proof-shell-wait)
- (decf jumps))
+ (cl-decf jumps))
((and (eq random-thing 1)
(not (proof-locked-region-empty-p)))
@@ -223,7 +224,7 @@ completely processing the buffer as the last step."
" random jump: retracting whole buffer")
(proof-retract-buffer)
(proof-shell-wait)
- (decf jumps))
+ (cl-decf jumps))
(t
(pg-autotest-message
@@ -241,7 +242,7 @@ completely processing the buffer as the last step."
" random jump: interrupting prover")
(proof-interrupt-process)))
(proof-shell-wait))
- (decf jumps)))))
+ (cl-decf jumps)))))
(unless (proof-locked-region-full-p)
(proof-process-buffer)
(proof-shell-wait))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 9be95972..755d41f5 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.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
@@ -30,6 +30,7 @@
;;
;;; Code:
+(eval-when-compile (require 'cl-lib))
(eval-when-compile
(require 'span)
(require 'unicode-tokens))
@@ -72,7 +73,7 @@
(t "command")))
(label (span-property span 'rawname))
(frameid (int-to-string pg-movie-frame)))
- (incf pg-movie-frame)
+ (cl-incf pg-movie-frame)
(pg-xml-node frame
(list (pg-xml-attr frameNumber frameid))
(list
diff --git a/generic/pg-user.el b/generic/pg-user.el
index a5ed27a9..57d29f18 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -558,18 +558,18 @@ last use time, to discourage saving these into the users database."
(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)))
+ (when proof-assistant
+ (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))))
;; 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) ;FIXME: Yuck!
- (eval-after-load "completion"
- '(proof-add-completions)))
+(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'."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 4c56fc7b..f8cf0cab 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,4 +1,4 @@
-;;; proof-script.el --- Major mode for proof assistant script files.
+;;; proof-script.el --- Major mode for proof assistant script files. -*- lexical-binding:t -*-
;; This file is part of Proof General.
@@ -42,6 +42,7 @@
(declare-function proof-segment-up-to "proof-script")
(declare-function proof-autosend-enable "pg-user")
(declare-function proof-interrupt-process "pg-shell")
+(declare-function proof-cd-sync "pg-user" ())
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;
@@ -142,7 +143,7 @@ scripting buffer may have an active queue span.")
;; ** Getters and setters
-(defun proof-span-give-warning (&rest args)
+(defun proof-span-give-warning (&rest _args)
"Give a warning message.
Optional argument ARGS is ignored."
(unless inhibit-read-only
@@ -506,7 +507,7 @@ Intended as a hook function for `proof-shell-handle-error-or-interrupt-hook'."
(defun pg-clear-script-portions ()
"Clear record of script portion names and types from internal list."
(dolist (idtbl pg-script-portions)
- (maphash (lambda (k span) (span-delete span)) (cdr idtbl))
+ (maphash (lambda (_k span) (span-delete span)) (cdr idtbl))
(clrhash (cdr idtbl))))
(defun pg-remove-element (idiom id)
@@ -628,14 +629,11 @@ IDIOMSYM is a symbol and ID is a strings."
(concat "Make "
(if current-prefix-arg "in" "")
"visible all regions of: ")
- (apply 'vector pg-idioms) nil t))
+ (apply #'vector pg-idioms) nil t))
current-prefix-arg))
(let ((elts (cdr-safe (assq idiom pg-script-portions)))
- (alterfn (if hide
- (lambda (k span)
- (pg-set-element-span-invisible span t))
- (lambda (k span)
- (pg-set-element-span-invisible span nil)))))
+ (alterfn (lambda (_k span)
+ (pg-set-element-span-invisible span hide))))
(when elts
(proof-with-script-buffer ; may be called from menu
(maphash alterfn elts)))))
@@ -668,7 +666,6 @@ Each span has a 'type property, one of:
'pbp A PBP command inserted automatically into the script."
(let ((type (span-property span 'type))
(idiom (span-property span 'idiom))
- (name (span-property span 'name))
(rawname (span-property span 'rawname)))
(cond
(idiom
@@ -1213,10 +1210,10 @@ activation is considered to have failed and an error is given."
;; If there's another buffer currently active, we need to
;; deactivate it (also fixing up the included files list).
(when proof-script-buffer
- (proof-deactivate-scripting)
- ;; Test whether deactivation worked
- (if proof-script-buffer
- (error
+ (proof-deactivate-scripting)
+ ;; Test whether deactivation worked
+ (if proof-script-buffer
+ (error
"You cannot have more than one active scripting buffer!")))
;; Ensure this buffer is off the included files list. If we
@@ -1265,21 +1262,21 @@ activation is considered to have failed and an error is given."
;; block. NB: The hook function may send commands to the
;; process which will re-enter this function, but should exit
;; immediately because scripting has been turned on now.
- (if proof-activate-scripting-hook
- (let
- ((activated-interactively (called-interactively-p 'any)))
- (setq proof-shell-last-output-kind nil)
- (run-hooks 'proof-activate-scripting-hook)
- ;; If activate scripting functions caused an error,
- ;; prevent switching to another buffer. Might be better
- ;; to leave to specific instances, or simply run the hooks
- ;; as the last step before turning on scripting properly.
- (when (or (eq 'error proof-shell-last-output-kind)
- (eq 'interrupt proof-shell-last-output-kind))
- (proof-deactivate-scripting) ;; turn off again!
- ;; Give an error to prevent further actions.
- (error
- "Scripting not activated because of error or interrupt")))))))
+ (when proof-activate-scripting-hook
+ (defvar activated-interactively)
+ (let ((activated-interactively (called-interactively-p 'any)))
+ (setq proof-shell-last-output-kind nil)
+ (run-hooks 'proof-activate-scripting-hook)
+ ;; If activate scripting functions caused an error,
+ ;; prevent switching to another buffer. Might be better
+ ;; to leave to specific instances, or simply run the hooks
+ ;; as the last step before turning on scripting properly.
+ (when (or (eq 'error proof-shell-last-output-kind)
+ (eq 'interrupt proof-shell-last-output-kind))
+ (proof-deactivate-scripting) ;; turn off again!
+ ;; Give an error to prevent further actions.
+ (error
+ "Scripting not activated because of error or interrupt")))))))
(defun proof-toggle-active-scripting (&optional arg)
@@ -1415,7 +1412,8 @@ Argument SPAN has just been processed."
(span-end span)))
(if (proof-string-match-safe proof-script-evaluate-elisp-comment-regexp str)
(condition-case nil
- (eval (car (read-from-string (match-string-no-properties 1 str))))
+ (eval (car (read-from-string (match-string-no-properties 1 str)))
+ t)
(t (proof-debug
(concat
"lisp error when obeying proof-shell-evaluate-elisp-comment-regexp: \n"
@@ -1599,7 +1597,7 @@ Subroutine of `proof-done-advancing-save'."
;; start of the buffer, we make a fake goal-save region.
;; Delete spans between the previous goal and new command
- (mapc 'span-delete dels)
+ (mapc #'span-delete dels)
;; Try to set the name from the goal... [as above]
(setq nam (or (proof-get-name-from-goal gspan)
@@ -1643,7 +1641,7 @@ Subroutine of `proof-done-advancing-save'."
;; command syntax (terminated, not terminated, or lisp-style), whether
;; or not PG silently ignores comments, etc.
-(defun proof-segment-up-to-parser (pos &optional next-command-end)
+(defun proof-segment-up-to-parser (pos &optional _next-command-end)
"Parse the script buffer from end of queue/locked region to POS.
This partitions the script buffer into contiguous regions, classifying
them by type. Return a list of lists of the form
@@ -1838,7 +1836,7 @@ The optional QUEUEFLAGS are added to each queue item."
(let ((start (proof-queue-or-locked-end))
(file (or (buffer-file-name) (buffer-name)))
(cb 'proof-done-advancing)
- span alist semi item end)
+ span alist end)
(setq semis (nreverse semis))
(save-match-data
(dolist (semi semis)
@@ -1927,7 +1925,7 @@ always defaults to inserting a semi (nicer might be to parse for a
comment, and insert or skip to the next semi)."
(let ((mrk (point))
(termregexp (regexp-quote proof-terminal-string))
- ins incomment nwsp)
+ ins nwsp)
(if (< mrk (proof-unprocessed-begin))
(insert proof-terminal-string) ; insert immediately in locked region
(if (proof-only-whitespace-to-locked-region-p)
@@ -1953,7 +1951,6 @@ comment, and insert or skip to the next semi)."
(unless semis
(error "Can't find a parseable command!"))
(when (eq 'unclosed-comment (caar semis))
- (setq incomment t)
;; delete spurious char in comment
(if ins (backward-delete-char 1))
(goto-char mrk)
@@ -2258,17 +2255,22 @@ query saves here."
;; Proof General scripting mode definition, part 1.
;;
+(defvar proof--splash-done nil)
+
;;;###autoload
(define-derived-mode proof-mode fundamental-mode
proof-general-name
"Proof General major mode class for proof scripts.
\\{proof-mode-map}"
+ (unless (or proof--splash-done noninteractive)
+ (setq proof--splash-done t)
+ (proof-splash-message))
+
(setq proof-buffer-type 'script)
;; Set default indent function (can be overriden in derived modes)
- (make-local-variable 'indent-line-function)
- (setq indent-line-function 'proof-indent-line)
+ (setq-local indent-line-function #'proof-indent-line)
;; During write-file it can happen that we re-set the mode for the
;; currently active scripting buffer. The user might also do this
@@ -2286,9 +2288,9 @@ query saves here."
(proof-script-set-after-change-functions)
(add-hook 'after-set-visited-file-name-hooks
- 'proof-script-set-visited-file-name nil t)
+ #'proof-script-set-visited-file-name nil t)
- (add-hook 'proof-activate-scripting-hook 'proof-cd-sync nil t))
+ (add-hook 'proof-activate-scripting-hook #'proof-cd-sync nil t))
;; NB: proof-mode-map declared above
(proof-menu-define-keys proof-mode-map)
@@ -2321,9 +2323,9 @@ This hook also gives a warning in case this is the active scripting buffer."
"Set the hooks for a proof script buffer.
The hooks set here are cleared by `write-file', so we use this function
to restore them using `after-set-visited-file-name-hooks'."
- (add-hook 'kill-buffer-hook 'proof-script-kill-buffer-fn t t)
+ (add-hook 'kill-buffer-hook #'proof-script-kill-buffer-fn t t)
;; Reverting buffer is same as killing it as far as PG is concerned
- (add-hook 'before-revert-hook 'proof-script-kill-buffer-fn t t))
+ (add-hook 'before-revert-hook #'proof-script-kill-buffer-fn t t))
(defun proof-script-kill-buffer-fn ()
"Value of `kill-buffer-hook' for proof script buffers.
@@ -2616,17 +2618,17 @@ finish setup which depends on specific proof assistant configuration."
"Choose parsing mechanism according to different kinds of script syntax.
Choice of function depends on configuration setting."
(unless (fboundp 'proof-segment-up-to)
- (defalias 'proof-segment-up-to 'proof-segment-up-to-parser)
+ (defalias 'proof-segment-up-to #'proof-segment-up-to-parser)
(cond
(proof-script-parse-function
;; already set, nothing to do
)
(proof-script-sexp-commands
- (setq proof-script-parse-function 'proof-script-generic-parse-sexp))
+ (setq proof-script-parse-function #'proof-script-generic-parse-sexp))
(proof-script-command-start-regexp
- (setq proof-script-parse-function 'proof-script-generic-parse-cmdstart))
+ (setq proof-script-parse-function #'proof-script-generic-parse-cmdstart))
((or proof-script-command-end-regexp proof-terminal-string)
- (setq proof-script-parse-function 'proof-script-generic-parse-cmdend)
+ (setq proof-script-parse-function #'proof-script-generic-parse-cmdend)
(unless proof-script-command-end-regexp
(proof-warn-if-unset "probof-config-done" 'proof-terminal-string)
(setq proof-script-command-end-regexp
@@ -2726,7 +2728,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
(cdr semis))))
usedsemis)))
-(defun proof-script-after-change-function (start end prelength)
+(defun proof-script-after-change-function (start _end _prelength)
"Value for `after-change-functions' in proof script buffers."
(setq proof-last-edited-low-watermark
(min (or proof-last-edited-low-watermark (point-max))
@@ -2741,7 +2743,7 @@ Stores recent results of `proof-segment-up-to' in reverse order.")
(defun proof-script-set-after-change-functions ()
"Set `after-change-functions' for script buffers."
(add-hook 'after-change-functions
- 'proof-script-after-change-function nil t))
+ #'proof-script-after-change-function nil t))
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index 75164890..600e9b4e 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.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
@@ -270,7 +270,7 @@ binding to remove this buffer."
(defun proof-splash-message ()
"Make sure the user gets welcomed one way or another."
(interactive)
- (unless (or proof-splash-seen noninteractive (bound-and-true-p byte-compile-current-file))
+ (unless (or proof-splash-seen noninteractive)
(if proof-splash-enable
(progn
;; disable ordinary emacs splash
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index e93f5ca4..d494279a 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -36,18 +36,14 @@ Uses a regexp of the form \\_<...\\_>."
(defconst proof-no-regexp "\\<\\>"
"A regular expression that never matches anything.")
-(defsubst proof-regexp-alt (&rest args)
+(defsubst proof-regexp-alt-list (args)
"Return the regexp which matches any of the regexps ARGS."
- ;; see regexp-opt (NB: but that is for strings, not regexps)
- (let ((res ""))
- (dolist (regexp args)
- (setq res (concat res (if (string-equal res "") "\\(?:" "\\|\\(?:")
- regexp "\\)")))
- res))
+ (mapconcat #'identity args "\\|"))
-(defsubst proof-regexp-alt-list (args)
+(defsubst proof-regexp-alt (&rest args)
"Return the regexp which matches any of the regexps ARGS."
- (apply 'proof-regexp-alt args))
+ ;; see regexp-opt (NB: but that is for strings, not regexps)
+ (proof-regexp-alt-list args))
(defsubst proof-re-search-forward-region (startre endre)
"Search for a region delimited by regexps STARTRE and ENDRE.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 9a60e0ac..4ce51c99 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.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
@@ -50,7 +50,7 @@ approximation we test whether proof-config is fully-loaded yet."
(set-default sym value)
(when (and
(not noninteractive)
- (not (bound-and-true-p byte-compile-current-file))
+ (not (bound-and-true-p byte-compile-current-file)) ;FIXME: Yuck!
(featurep 'pg-custom)
(featurep 'proof-config))
(if (fboundp sym)
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 99e537c5..1568b2f0 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -23,6 +23,7 @@
;;; Code:
+(eval-when-compile (require 'cl-lib))
;;
;; Give Emacs version mismatch error here.
;;
@@ -58,8 +59,6 @@
(require 'proof-autoloads) ; interface fns
(require 'scomint) ; for proof-shell-live-buffer
-;;; Code:
-
;;
;; Handy macros
;;
@@ -247,7 +246,8 @@ Experimentally we display a message from time to time advertising
;; IF there *isn't* a visible window showing buffer...
(unless (get-buffer-window buffer 0)
(if proof-three-window-enable
- (if (< proof-advertise-layout-count 30) (incf proof-advertise-layout-count)
+ (if (< proof-advertise-layout-count 30)
+ (cl-incf proof-advertise-layout-count)
(message (substitute-command-keys "Hit \\[proof-layout-windows] to reset layout"))
(setq proof-advertise-layout-count 0)))
;; THEN either we are in 2 wins mode and we must switch the assoc
diff --git a/generic/proof.el b/generic/proof.el
index f3b3b276..769459df 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -1,4 +1,4 @@
-;;; proof.el --- Proof General theorem prover interface
+;;; proof.el --- Proof General theorem prover interface -*- lexical-binding:t -*-
;; This file is part of Proof General.
@@ -33,9 +33,6 @@
(require 'proof-site) ; site/prover config, global vars, autoloads
-(unless (or noninteractive (bound-and-true-p byte-compile-current-file))
- (proof-splash-message)) ; welcome the user now.
-
(require 'proof-utils) ; utilities
(require 'proof-config) ; configuration variables
(require 'proof-auxmodes) ; auxmode functions
diff --git a/obsolete/plastic/plastic.el b/obsolete/plastic/plastic.el
index cf69a731..39f6c01f 100644
--- a/obsolete/plastic/plastic.el
+++ b/obsolete/plastic/plastic.el
@@ -546,8 +546,8 @@ For Plastic, we assume that module identifiers coincide with file names."
(aset string i ?\ )
(cl-incf i) )))
(keep-rest (lambda ()
- (loop for x in (string-to-list plastic-lit-string)
- do (aset string i ?\ ) (cl-incf i))
+ (cl-loop for x in (string-to-list plastic-lit-string)
+ do (aset string i ?\ ) (cl-incf i))
(while (and (< i l)
(/= (aref string i) ?\n)
(/= (aref string i) ?-))
--
2.11.0
_______________________________________________
ProofGeneral-devel mailing list
ProofGeneral-devel@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/proofgeneral-devel
