diff options
| -rw-r--r-- | coq/coq-autotest.el | 4 | ||||
| -rw-r--r-- | coq/coq-db.el | 6 | ||||
| -rw-r--r-- | coq/coq.el | 3 | ||||
| -rw-r--r-- | generic/proof-shell.el | 23 |
4 files changed, 19 insertions, 17 deletions
diff --git a/coq/coq-autotest.el b/coq/coq-autotest.el index 3158ccd1..f803b852 100644 --- a/coq/coq-autotest.el +++ b/coq/coq-autotest.el @@ -5,7 +5,9 @@ ;; $Id$ ;; -(require 'cl) +(eval-when-compile + (require 'cl)) + (eval-when (compile) (require 'proof-site) (proof-ready-for-assistant 'coq)) diff --git a/coq/coq-db.el b/coq/coq-db.el index c063b6dd..4b8d53cd 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -14,7 +14,9 @@ ;;; Code: -(require 'cl) +(eval-when-compile + (require 'cl)) + (require 'proof-config) ; for proof-face-specs, a macro (require 'holes) @@ -171,7 +173,7 @@ for DB structure." Submenus contain SIZE entries (default 30). See `coq-syntax-db' for DB structure." ;; sort is destructive for the list, so copy list before sorting - (let* ((l (coq-sort-menu-entries (copy-list db))) (res ()) + (let* ((l (coq-sort-menu-entries (copy-sequence db))) (res ()) (wdth (+ 2 (max-length-db db))) (sz (or size 30)) (lgth (length l))) (while l @@ -11,8 +11,7 @@ ;; ;;; History: -(eval-when-compile - (require 'cl)) +(require 'cl) (eval-when (compile) (require 'proof-utils) diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 5eebdad5..3004c811 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -873,6 +873,17 @@ track what happens in the proof queue." "Insert ITEM from `proof-action-list' into the proof shell." (proof-shell-insert (nth 1 item) (nth 2 item) (nth 0 item))) +(defsubst proof-shell-slurp-comments () + "Strip comments at front of `proof-action-list', returning items stripped. +Comments are not sent to the prover." + (let (cbitems nextitem) + (while (and proof-action-list + (not (nth 1 (setq nextitem + (car proof-action-list))))) + (setq cbitems (cons nextitem cbitems)) + (setq proof-action-list (cdr proof-action-list))) + (nreverse cbitems))) + (defun proof-add-to-queue (queueitems &optional queuemode) "Chop off the vacuous prefix of the QUEUEITEMS and queue them. For each item with a nil command at the head of the list, invoke its @@ -950,18 +961,6 @@ The queue mode is set to 'advancing" (proof-set-queue-endpoints (proof-unprocessed-begin) end) (proof-add-to-queue queueitems 'advancing)) -(defsubst proof-shell-slurp-comments () - "Strip comments at front of `proof-action-list', returning items stripped. -Comments are not sent to the prover." - (let (cbitems nextitem) - (while (and proof-action-list - (not (nth 1 (setq nextitem - (car proof-action-list))))) - (setq cbitems (cons nextitem cbitems)) - (setq proof-action-list (cdr proof-action-list))) - (nreverse cbitems))) - - (defun proof-shell-exec-loop () "Process the `proof-action-list'. |