[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[nongnu] elpa/proof-general 91ce5cd 3/4: * coq/*.el: Use lexical-binding
|
From: |
ELPA Syncer |
|
Subject: |
[nongnu] elpa/proof-general 91ce5cd 3/4: * coq/*.el: Use lexical-binding plus various minor changes |
|
Date: |
Fri, 13 Aug 2021 17:57:37 -0400 (EDT) |
branch: elpa/proof-general
commit 91ce5cdec5ae4f4a00ea7411aea67d347895bef4
Author: Stefan Monnier <monnier@iro.umontreal.ca>
Commit: Stefan Monnier <monnier@iro.umontreal.ca>
* coq/*.el: Use lexical-binding plus various minor changes
Fit docstrings within 80 columns. Prefer #' to quote function names.
* coq/coq.el: Use lexical-binding.
(proof-shell-process-urgent-message-default): Remove deadcode.
(coq-set-auto-adapt-printing-width): Fix longstanding confusion between
`set` and `setq`.
(coq--show-proof-stepwise-cmds): New function.
(coq-empty-action-list-command): Use it. Avoid `add-to-list` on
local variables.
(coq-guess-goal-buffer-at-next-command): Fix longstanding paren typo.
(coq-proof-tree-get-new-subgoals): Use `push`.
(coq-shell-theorem-dependency-list-regexp): Use `defconst`.
(coq-dependency-menu-system-specific): Prefer closures over `(lambda..).
* coq/coq-unicode-tokens.el: Use lexical-binding.
(coq-control-region-format-regexp): Remove ineffective backslashes.
* coq/coq-system.el (coq-autodetect-help): Simplify.
* coq/coq-syntax.el (coq-queries-commands-db): Fix docstring within
80 columns.
* coq/coq-smie.el (coq-smie-search-token-backward):
Remove longstanding deadcode and optimize a bit.
(coq-smie-backward-token-aux): Re-layout a bit to fit within 80 columns.
(coq-show-smie--parent): Simplify.
(coq-smie-rules): Pass second arg to `looking-back` to avoid
pathological performance.
* coq/coq-seq-compile.el: Use lexical-binding.
(coq-seq-auto-compile-externally):
Rename arg `qualified-id` to avoid dynbound name.
Mark as dynbound those vars passed to `coq-compile-substitution-list`.
(coq-seq-preprocess-require-commands): Declare `coq-object-hash-symbol`
as dynbound.
* coq/coq-par-compile.el: Use lexical-binding.
(coq-par-coqdep-arguments, coq-par-coqc-arguments, coq-par-job-init-common)
(coq-par-create-require-job, coq-par-create-file-job):
Rename arg `coq-load-path` to avoid dynbound name.
(coq-par-retire-top-level-job, coq-par-kickoff-queue-maybe)
(coq-par-handle-require-list):
Prefer closures over `(lambda...).
* coq/coq-diffs.el: Use lexical-binding.
* coq/coq-compile-common.el: Use lexical-binding.
Remove redundant `:group`.
(coq-display-compile-response-buffer): Avoid deprecated
`font-lock-fontify-buffer`.
---
coq/coq-compile-common.el | 81 +++++-------
coq/coq-diffs.el | 2 +-
coq/coq-indent.el | 6 +-
coq/coq-par-compile.el | 91 ++++++-------
coq/coq-seq-compile.el | 80 ++++++------
coq/coq-smie.el | 35 ++---
coq/coq-syntax.el | 6 +-
coq/coq-system.el | 14 +-
coq/coq-unicode-tokens.el | 10 +-
coq/coq.el | 324 ++++++++++++++++++++++------------------------
10 files changed, 316 insertions(+), 333 deletions(-)
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 10eae53..8d836b6 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -1,9 +1,9 @@
-;;; coq-compile-common.el --- common part of compilation feature
+;;; coq-compile-common.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017, 2019-2021 Hendrik Tews
@@ -47,33 +47,33 @@
"Enable parallel compilation.
Must be used together with `coq-seq-disable'."
(add-hook 'proof-shell-extend-queue-hook
- 'coq-par-preprocess-require-commands)
+ #'coq-par-preprocess-require-commands)
(add-hook 'proof-shell-signal-interrupt-hook
- 'coq-par-user-interrupt)
+ #'coq-par-user-interrupt)
(add-hook 'proof-shell-handle-error-or-interrupt-hook
- 'coq-par-user-interrupt))
+ #'coq-par-user-interrupt))
(defun coq-par-disable ()
"Disable parallel compilation.
Must be used together with `coq-seq-enable'."
(remove-hook 'proof-shell-extend-queue-hook
- 'coq-par-preprocess-require-commands)
+ #'coq-par-preprocess-require-commands)
(remove-hook 'proof-shell-signal-interrupt-hook
- 'coq-par-user-interrupt)
+ #'coq-par-user-interrupt)
(remove-hook 'proof-shell-handle-error-or-interrupt-hook
- 'coq-par-user-interrupt))
+ #'coq-par-user-interrupt))
(defun coq-seq-enable ()
"Enable sequential synchronous compilation.
Must be used together with `coq-par-disable'."
(add-hook 'proof-shell-extend-queue-hook
- 'coq-seq-preprocess-require-commands))
+ #'coq-seq-preprocess-require-commands))
(defun coq-seq-disable ()
"Disable sequential synchronous compilation.
Must be used together with `coq-par-enable'."
(remove-hook 'proof-shell-extend-queue-hook
- 'coq-seq-preprocess-require-commands))
+ #'coq-seq-preprocess-require-commands))
@@ -173,8 +173,7 @@ are compiled from the sources before the \"Require\"
command is processed.
This option can be set/reset via menu
`Coq -> Auto Compilation -> Compile Before Require'."
:type 'boolean
- :safe 'booleanp
- :group 'coq-auto-compile)
+ :safe 'booleanp)
(proof-deftoggle coq-compile-before-require)
@@ -192,8 +191,7 @@ is set with `coq-max-background-compilation-jobs'.
This option can be set/reset via menu
`Coq -> Auto Compilation -> Compile Parallel In Background'."
:type 'boolean
- :safe 'booleanp
- :group 'coq-auto-compile)
+ :safe 'booleanp)
(proof-deftoggle coq-compile-parallel-in-background)
@@ -272,10 +270,9 @@ This option can be set via menu
(const :tag "use -quick, don't do vio2vo" quick-no-vio2vo)
(const :tag "use -quick and do vio2vo" quick-and-vio2vo)
(const :tag "ensure vo compilation, delete vio files" ensure-vo))
- :safe (lambda (v) (member v '(no-quick quick-no-vio2vo
- quick-and-vio2vo ensure-vo)))
- :set 'coq-compile-quick-setter
- :group 'coq-auto-compile)
+ :safe (lambda (v)
+ (member v '(no-quick quick-no-vio2vo quick-and-vio2vo ensure-vo)))
+ :set #'coq-compile-quick-setter)
(defun coq-compile-prefer-quick ()
"Return t if a .vio file would be prefered."
@@ -316,8 +313,7 @@ For coq < 8.11 this option is ignored."
(const :tag "use -vos, don't do -vok" vos)
(const :tag "use -vos and do -vok" vos-and-vok)
(const :tag "ensure vo compilation" ensure-vo))
- :safe (lambda (v) (member v '(nil vos vos-and-vok ensure-vo)))
- :group 'coq-auto-compile)
+ :safe (lambda (v) (member v '(nil vos vos-and-vok ensure-vo))))
(defun coq-compile-prefer-vos ()
"Decide whether ``-vos'' should be used.
@@ -354,8 +350,7 @@ is not adapted."
:type '(choice (const :tag "use all CPU cores" all-cpus)
(integer :tag "fixed number" :value 1))
:safe (lambda (v) (or (eq v 'all-cpus) (and (integerp v) (> v 0))))
- :set 'coq-max-jobs-setter
- :group 'coq-auto-compile)
+ :set #'coq-max-jobs-setter)
(defcustom coq-max-background-second-stage-percentage
(or (and (boundp 'coq-max-background-vio2vo-percentage)
@@ -374,16 +369,14 @@ is initialized from the now deprecated option
`coq-max-background-vio2vo-percentage'."
:type 'number
:safe 'numberp
- :set 'coq-max-second-stage-setter
- :group 'coq-auto-compile)
+ :set #'coq-max-second-stage-setter)
(defcustom coq-max-background-vio2vo-percentage nil
"Deprecated. Please configure `coq-max-background-second-stage-percentage'.
This is the old configuration option for Coq < 8.11, used before
the ``-vok'' second stage was implemented."
:type 'number
- :safe 'numberp
- :group 'coq-auto-compile)
+ :safe 'numberp)
(defcustom coq-compile-second-stage-delay
@@ -401,8 +394,7 @@ For backward compatibility, if this option is not
customized, it
is initialized from the now deprecated option
`coq-compile-vio2vo-delay'."
:type 'number
- :safe 'numberp
- :group 'coq-auto-compile)
+ :safe 'numberp)
(defcustom coq-compile-vio2vo-delay nil
;; XXX replace coq-compile-vio2vo-delay in ../doc/ProofGeneral.texi
@@ -410,8 +402,7 @@ is initialized from the now deprecated option
This is the old configuration option for Coq < 8.11, used before
the ``-vok'' second stage was implemented."
:type 'number
- :safe 'numberp
- :group 'coq-auto-compile)
+ :safe 'numberp)
(defcustom coq-compile-command ""
"External compilation command. If empty ProofGeneral compiles itself.
@@ -440,8 +431,7 @@ minibuffer if `coq-confirm-external-compilation' is t."
:safe (lambda (v)
(and (stringp v)
(or (not (boundp 'coq-confirm-external-compilation))
- coq-confirm-external-compilation)))
- :group 'coq-auto-compile)
+ coq-confirm-external-compilation))))
(defconst coq-compile-substitution-list
'(("%p" physical-dir)
@@ -454,9 +444,9 @@ Value must be a list of substitutions, where each
substitution is
a 2-element list. The first element of a substitution is the
regexp to substitute, the second the replacement. The replacement
is evaluated before passing it to `replace-regexp-in-string', so
-it might be a string, or one of the symbols 'physical-dir,
-'module-object, 'module-source, 'qualified-id and
-'requiring-file, which are bound to, respectively, the physical
+it might be a string, or one of the symbols `physical-dir',
+`module-object', `module-source', `qualified-id' and
+`requiring-file', which are bound to, respectively, the physical
directory containing the source file, the Coq object file in
'physical-dir that will be loaded, the Coq source file in
'physical-dir whose object will be loaded, the qualified module
@@ -489,8 +479,7 @@ This option can be set via menu
"save all coq-mode buffers except the current buffer without confirmation"
save-coq)
(const :tag "save all buffers without confirmation" save-all))
- :safe (lambda (v) (member v '(ask-coq ask-all save-coq save-all)))
- :group 'coq-auto-compile)
+ :safe (lambda (v) (member v '(ask-coq ask-all save-coq save-all))))
(defcustom coq-lock-ancestors t
"If non-nil, lock ancestor module files.
@@ -502,8 +491,7 @@ This option can be set via menu
`Coq -> Auto Compilation -> Lock Ancestors'."
:type 'boolean
- :safe 'booleanp
- :group 'coq-auto-compile)
+ :safe 'booleanp)
;; define coq-lock-ancestors-toggle
(proof-deftoggle coq-lock-ancestors)
@@ -516,8 +504,7 @@ Otherwise start the external compilation without
confirmation.
This option can be set/reset via menu
`Coq -> Auto Compilation -> Confirm External Compilation'."
- :type 'boolean
- :group 'coq-auto-compile)
+ :type 'boolean)
(defcustom coq-compile-ignored-directories nil
@@ -533,8 +520,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) (cl-every #'stringp v))
- :group 'coq-auto-compile)
+ :safe (lambda (v) (cl-every #'stringp v)))
(defcustom coq-coqdep-error-regexp
(concat "^\\*\\*\\* Warning: in file .*, library .* is required "
@@ -550,8 +536,7 @@ library at multiple places in the load path. If you want
to turn
the latter condition into an error, then set this variable to
\"^\\*\\*\\* Warning\"."
:type 'string
- :safe 'stringp
- :group 'coq-auto-compile)
+ :safe 'stringp)
(defconst coq-require-id-regexp
@@ -675,7 +660,7 @@ Changes the suffix from .vo to .vok. VO-OBJ-FILE must have
a .vo suffix."
(defun coq-unlock-all-ancestors-of-span (span)
"Unlock all ancestors that have been locked when SPAN was asserted."
- (mapc 'coq-unlock-ancestor (span-property span 'coq-locked-ancestors))
+ (mapc #'coq-unlock-ancestor (span-property span 'coq-locked-ancestors))
(span-set-property span 'coq-locked-ancestors ()))
@@ -732,7 +717,9 @@ the command whose output will appear in the buffer."
(with-current-buffer coq--compile-response-buffer
;; fontification enables the error messages
(let ((font-lock-verbose nil)) ; shut up font-lock messages
- (font-lock-fontify-buffer)))
+ (if (fboundp 'font-lock-ensure)
+ (font-lock-ensure)
+ (with-no-warnings (font-lock-fontify-buffer)))))
;; Make it so the next C-x ` will use this buffer.
(setq next-error-last-buffer (get-buffer coq--compile-response-buffer))
(proof-display-and-keep-buffer coq--compile-response-buffer 1 t)
diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index ff71634..f623324 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -1,4 +1,4 @@
-;;; coq-diffs.el --- highlight text marked with XML-like tags for Coq diffs
+;;; coq-diffs.el --- highlight text marked with XML-like tags for Coq diffs
-*- lexical-binding: t; -*-
;; This file is part of Proof General.
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index e064981..3a531e5 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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -188,8 +188,8 @@ There are 3 substrings (2 and 3 may be nil):
* number 2 is the left context matched that is not part of the ending string
* number 3 is the right context matched that is not part of the ending string
-Remark: This regexp is much more precise than `coq-end-command-regexp-forward'
but only
-works when searching backward.")
+Remark: This regexp is much more precise than `coq-end-command-regexp-forward'
+but only works when searching backward.")
(defun coq-search-comment-delimiter-forward ()
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 1e2d757..a7a3ae6 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -1,9 +1,9 @@
-;;; coq-par-compile.el --- parallel compilation of required modules
+;;; coq-par-compile.el --- parallel compilation of required modules -*-
lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017, 2019-2021 Hendrik Tews
@@ -734,10 +734,10 @@ If no circle is found return nil, otherwise the list of
files
belonging to the circle. Jobs in state 'enqueue-coqc can be
ignored, because they can never participate in a cycle."
(let (cycle)
- (maphash (lambda (key job) (put job 'visited nil))
+ (maphash (lambda (_key job) (put job 'visited nil))
coq--compilation-object-hash)
(maphash
- (lambda (key job)
+ (lambda (_key job)
(when (and (not cycle) (not (get job 'visited))
(eq (get job 'state) 'waiting-dep))
(setq cycle (coq-par-find-dependency-circle-for-job job nil))))
@@ -747,22 +747,22 @@ ignored, because they can never participate in a cycle."
;;; map coq module names to files, using synchronously running coqdep
-(defun coq-par-coqdep-arguments (lib-src-file coq-load-path)
+(defun coq-par-coqdep-arguments (lib-src-file clpath)
"Compute the command line arguments for invoking coqdep on LIB-SRC-FILE.
-Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
+Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (coq-coqdep-prog-args coq-load-path
+ (nconc (coq-coqdep-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
(list lib-src-file)))
-(defun coq-par-coqc-arguments (lib-src-file coq-load-path)
+(defun coq-par-coqc-arguments (lib-src-file clpath)
"Compute the command line arguments for invoking coqc on LIB-SRC-FILE.
-Argument COQ-LOAD-PATH must be `coq-load-path' from the buffer
+Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
load-path options to coqdep."
- (nconc (coq-coqc-prog-args coq-load-path (file-name-directory lib-src-file)
(coq--pre-v85))
+ (nconc (coq-coqc-prog-args clpath (file-name-directory lib-src-file)
(coq--pre-v85))
(list lib-src-file)))
(defun coq-par-analyse-coq-dep-exit (status output command)
@@ -786,7 +786,7 @@ or .vos files must be done elsewhere."
(progn
;; display the error
(coq-compile-display-error
- (mapconcat 'identity command " ")
+ (mapconcat #'identity command " ")
(if (equal output "")
"No coqdep output - file probably inaccessible"
output)
@@ -849,7 +849,7 @@ Return t if some process was killed."
Used for unlocking ancestors on compilation errors."
(when coq--compilation-object-hash
(maphash
- (lambda (key job)
+ (lambda (_key job)
(when (eq (get job 'lock-state) 'locked)
(coq-unlock-ancestor (get job 'src-file))
(put job 'lock-state 'unlocked)))
@@ -948,14 +948,14 @@ file to be deleted when the process does not finish
successfully."
(when coq--debug-auto-compilation
(message "%s %s: start %s %s in %s"
(get job 'name) process-name
- command (mapconcat 'identity arguments " ")
+ command (mapconcat #'identity arguments " ")
default-directory))
(condition-case err
;; If the command is wrong, start-process aborts with an
;; error. However, in Emacs 23.4.1. it will leave a process
;; behind, which is in a very strange state: running with no
;; pid. Emacs 24.2 fixes this.
- (setq process (apply 'start-process process-name
+ (setq process (apply #'start-process process-name
nil ; no process buffer
command arguments))
(error
@@ -969,8 +969,8 @@ file to be deleted when the process does not finish
successfully."
(ignore-errors (delete-file file-rm)))
(signal 'coq-compile-error-command-start
(list (cons command arguments) (nth 2 err)))))
- (set-process-filter process 'coq-par-process-filter)
- (set-process-sentinel process 'coq-par-process-sentinel)
+ (set-process-filter process #'coq-par-process-filter)
+ (set-process-sentinel process #'coq-par-process-sentinel)
(set-process-query-on-exit-flag process nil)
(setq coq--current-background-jobs (1+ coq--current-background-jobs))
(process-put process 'coq-compilation-job job)
@@ -1056,7 +1056,7 @@ function and reported appropriately."
(let ((cycle (coq-par-find-dependency-circle)))
(if cycle
(signal 'coq-compile-error-circular-dep
- (mapconcat 'identity cycle " -> "))
+ (mapconcat #'identity cycle " -> "))
(error "Deadlock in parallel compilation"))))))
;; coq-compile-error-start can be signaled inside the continuation
;; function, if that tries to start new jobs
@@ -1115,7 +1115,7 @@ detect more than one active callback, see
(not (eq race-counter coq--par-second-stage-start-id)))
(setq coq--par-second-stage-delay-timer
(run-at-time coq-compile-second-stage-delay nil
- 'coq-par-run-second-stage-queue))))
+ #'coq-par-run-second-stage-queue))))
(defun coq-par-callback-queue-item (callback)
"Create queue item containing just CALLBACK.
@@ -1448,8 +1448,8 @@ cleared before the next collection run."
;; (mapconcat
;; (lambda (job) (get job 'name))
;; (get job 'coqc-dependees) " "))
- (apply 'nconc (mapcar 'coq-par-collect-locked-file-ancestors
- (get job 'coqc-dependees))))
+ (apply #'nconc (mapcar #'coq-par-collect-locked-file-ancestors
+ (get job 'coqc-dependees))))
(defun coq-par-collect-locked-file-ancestors (job)
"Collect locked, not-yet-found ancestors of JOB.
@@ -1543,8 +1543,8 @@ jobs when they transition from 'waiting-queue to 'ready:
(car items) ; this is the require
(cons
(coq-par-callback-queue-item
- `(lambda (span) (coq-par-require-processed
- ,2nd-stage-counter)))
+ (lambda (_span) (coq-par-require-processed
+ 2nd-stage-counter)))
(cdr items))))))
(proof-add-to-queue items 'advancing)
(when coq--debug-auto-compilation
@@ -1628,8 +1628,8 @@ retired and transition to 'ready. This means:
(setq coq--par-delayed-last-job t)
(proof-add-to-queue
(list (coq-par-callback-queue-item
- `(lambda (span)
- (coq-par-kickoff-queue-from-action-list ',job))))
+ (lambda (_span)
+ (coq-par-kickoff-queue-from-action-list job))))
'advancing))
(put job 'state 'ready)
(when coq--debug-auto-compilation
@@ -1686,7 +1686,7 @@ retired and transition to 'ready. This means:
"second stage timer set before last compilation
job")
(setq coq--par-second-stage-delay-timer
(run-at-time coq-compile-second-stage-delay nil
- 'coq-par-run-second-stage-queue))))
+ #'coq-par-run-second-stage-queue))))
(setq coq--last-compilation-job nil)
(setq proof-second-action-list-active nil)
(when coq--debug-auto-compilation
@@ -1793,12 +1793,12 @@ before."
(get job 'obj-mod-time))))
(put job 'youngest-coqc-dependency dep-time)
(when coq--debug-auto-compilation
- (let (ancs)
- (message "%s: kickoff %d coqc dependencies with time %s"
- (get job 'name) (length (get job 'coqc-dependants))
- (if (eq dep-time 'just-compiled)
- 'just-compiled
- (current-time-string dep-time)))))
+ ;; (let (ancs)
+ (message "%s: kickoff %d coqc dependencies with time %s"
+ (get job 'name) (length (get job 'coqc-dependants))
+ (if (eq dep-time 'just-compiled)
+ 'just-compiled
+ (current-time-string dep-time))))
;; In the recursion coq-par-kickoff-coqc-dependants ->
;; coq-par-decrease-coqc-dependency -> coq-par-compile-job-maybe
;; -> coq-par-kickoff-coqc-dependants jobs on the path upwards
@@ -1835,7 +1835,7 @@ was queued."
(get job 'load-path)))
(coq-load-path-include-current nil)
(require-command
- (mapconcat 'identity (nth 1 (car (get job 'queueitems))) " "))
+ (mapconcat #'identity (nth 1 (car (get job 'queueitems))) " "))
(temp-file (make-temp-file "ProofGeneral-coq" nil ".v")))
(put job 'temp-require-file temp-file)
(with-temp-file temp-file (insert require-command))
@@ -1984,7 +1984,7 @@ synchronously or asynchronously."
(coq-par-start-task new-job)
(coq-par-job-enqueue new-job)))
-(defun coq-par-job-init-common (coq-load-path type current-dir)
+(defun coq-par-job-init-common (clpath type current-dir)
"Common initialization for 'require and 'file jobs.
Create a new job of type TYPE and initialize all common fields of
require and file jobs that need an initialization different from
@@ -2000,13 +2000,13 @@ nil."
;; jobs, however, if the field is present, we can treat require
;; and file jobs more uniformely.
(put new-job 'youngest-coqc-dependency '(0 0))
- (put new-job 'load-path coq-load-path)
+ (put new-job 'load-path clpath)
new-job))
-(defun coq-par-create-require-job (coq-load-path require-items require-span
- current-dir)
+(defun coq-par-create-require-job (clpath require-items require-span
+ current-dir)
"Create a new require job for REQUIRE-SPAN.
-Create a new require job and initialize its fields. COQ-LOAD-PATH
+Create a new require job and initialize its fields. CLPATH
is the load path configured for the current scripting buffer,
that is passed down to all dependencies and used in all
compilations. REQUIRE-ITEMS are the non-require commands
@@ -2021,12 +2021,13 @@ compilation from a sentinel or elsewhere.
This function is called synchronously when asserting. The new
require job is neither started nor enqueued here - the caller
must do this."
- (let ((new-job (coq-par-job-init-common coq-load-path 'require current-dir)))
+ (let* ((coq-load-path clpath)
+ (new-job (coq-par-job-init-common clpath 'require current-dir)))
(put new-job 'require-span require-span)
(put new-job 'queueitems require-items)
(when coq--debug-auto-compilation
(let* ((require-item (car require-items))
- (require-command (mapconcat 'identity (nth 1 require-item) " ")))
+ (require-command (mapconcat #'identity (nth 1 require-item) " ")))
(message "%s: create require job for %s"
(get new-job 'name) require-command)))
new-job))
@@ -2035,7 +2036,7 @@ must do this."
;; there was some error and it was not used anywhere back then, but
;; job is now needed as a dependency of some other file?
;; XXX what happens if the job exists and is failed?
-(defun coq-par-create-file-job (module-vo-file coq-load-path dep-src-file
+(defun coq-par-create-file-job (module-vo-file clpath dep-src-file
current-dir)
"Create a new file job for MODULE-VO-FILE.
DEP-SRC-FILE is the source file whose coqdep output we are just
@@ -2053,7 +2054,8 @@ If a new job is created it is started or enqueued right
away."
(cond
((gethash module-vo-file coq--compilation-object-hash))
(t
- (let ((new-job (coq-par-job-init-common coq-load-path 'file current-dir)))
+ (let* ((coq-load-path clpath)
+ (new-job (coq-par-job-init-common clpath 'file current-dir)))
;; fields 'required-obj-file and obj-mod-time are implicitely set to nil
(put new-job 'vo-file module-vo-file)
(put new-job 'src-file (coq-library-src-of-vo-file module-vo-file))
@@ -2206,7 +2208,7 @@ behind PROCESS."
(coq-par-kickoff-coqc-dependants job t))
;; coqc error
(coq-compile-display-error
- (mapconcat 'identity (process-get process 'coq-process-command) " ")
+ (mapconcat #'identity (process-get process 'coq-process-command) " ")
(process-get process 'coq-process-output)
t)
(if coq-compile-keep-going
@@ -2283,8 +2285,7 @@ This function is called synchronously when asserting."
(message "handle require command \"%s\"" require-command)))
(span-add-delete-action
span
- `(lambda ()
- (coq-unlock-all-ancestors-of-span ,span)))
+ (lambda () (coq-unlock-all-ancestors-of-span span)))
;; create a new require job and maintain coq--last-compilation-job
(setq new-job
(coq-par-create-require-job coq-load-path require-items span
@@ -2302,7 +2303,7 @@ This function is called synchronously when asserting."
"Return t if ITEM contains a Require command.
Predicate for `split-list-at-predicate', used to split the new
queue items at each Require command."
- (let ((string (mapconcat 'identity (nth 1 item) " ")))
+ (let ((string (mapconcat #'identity (nth 1 item) " ")))
(and string
(string-match coq-require-command-regexp string))))
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 3cdcd02..d15a87e 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -1,9 +1,9 @@
-;;; coq-seq-compile.el --- sequential compilation of required modules
+;;; coq-seq-compile.el --- sequential compilation of required modules -*-
lexical-binding: t; -*-
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -84,7 +84,7 @@ break."
(message "call coqdep arg list: %S" coqdep-arguments))
(with-temp-buffer
(setq coqdep-status
- (apply 'call-process
+ (apply #'call-process
coq-dependency-analyzer nil (current-buffer) nil
coqdep-arguments))
(setq coqdep-output (buffer-string)))
@@ -100,7 +100,7 @@ break."
this-command)))
;; display the error
(coq-init-compile-response-buffer
- (mapconcat 'identity full-command " "))
+ (mapconcat #'identity full-command " "))
(let ((inhibit-read-only t))
(with-current-buffer coq--compile-response-buffer
(insert coqdep-output)))
@@ -120,11 +120,11 @@ Display errors in buffer `coq--compile-response-buffer'."
(list src-file)))
coqc-status)
(coq-init-compile-response-buffer
- (mapconcat 'identity (cons coq-compiler coqc-arguments) " "))
+ (mapconcat #'identity (cons coq-compiler coqc-arguments) " "))
(when coq--debug-auto-compilation
(message "call coqc arg list: %s" coqc-arguments))
(setq coqc-status
- (apply 'call-process
+ (apply #'call-process
coq-compiler nil coq--compile-response-buffer t
coqc-arguments))
(when coq--debug-auto-compilation
(message "compilation %s exited with %s, output |%s|"
@@ -243,8 +243,7 @@ function."
(puthash lib-obj-file result coq-obj-hash)
result)))
-(defun coq-seq-auto-compile-externally (span qualified-id
- absolute-module-obj-file)
+(defun coq-seq-auto-compile-externally (span q-id absolute-module-obj-file)
"Make MODULE up-to-date according to `coq-compile-command'.
Start a compilation to make ABSOLUTE-MODULE-OBJ-FILE up-to-date.
The compilation command is derived from `coq-compile-command' by
@@ -260,7 +259,14 @@ span for for proper unlocking on retract.
This function uses the low-level interface `compilation-start',
therefore the customizations for `compile' do not apply."
(unless (coq-compile-ignore-file absolute-module-obj-file)
+ ;; Dynvar list taken from `coq-compile-substitution-list'.
+ (defvar physical-dir)
+ (defvar module-object)
+ (defvar module-source)
+ (defvar qualified-id)
+ (defvar requiring-file)
(let* ((local-compile-command coq-compile-command)
+ (qualified-id q-id)
(physical-dir (file-name-directory absolute-module-obj-file))
(module-object (file-name-nondirectory absolute-module-obj-file))
(module-source (coq-library-src-of-vo-file module-object))
@@ -269,7 +275,7 @@ therefore the customizations for `compile' do not apply."
(lambda (substitution)
(setq local-compile-command
(replace-regexp-in-string
- (car substitution) (eval (car (cdr substitution)))
+ (car substitution) (eval (car (cdr substitution)) t)
local-compile-command)))
coq-compile-substitution-list)
(if coq-confirm-external-compilation
@@ -287,7 +293,7 @@ therefore the customizations for `compile' do not apply."
span
(coq-library-src-of-vo-file absolute-module-obj-file)))))
-(defun coq-seq-map-module-id-to-obj-file (module-id span &optional from)
+(defun coq-seq-map-module-id-to-obj-file (module-id _span &optional from)
"Map MODULE-ID to the appropriate coq object file.
The mapping depends of course on `coq-load-path'. The current
implementation invokes coqdep with a one-line require command.
@@ -363,7 +369,7 @@ will be used for all \"Require\" commands added at once to
the queue."
(if (> (length coq-compile-command) 0)
(coq-seq-auto-compile-externally span module-id module-obj-file)
(unless (symbol-value coq-object-local-hash-symbol)
- (set coq-object-local-hash-symbol (make-hash-table :test 'equal)))
+ (set coq-object-local-hash-symbol (make-hash-table :test #'equal)))
(coq-seq-make-lib-up-to-date (symbol-value
coq-object-local-hash-symbol)
span module-obj-file)))))
@@ -371,31 +377,33 @@ will be used for all \"Require\" commands added at once
to the queue."
"Coq function for `proof-shell-extend-queue-hook'.
If `coq-compile-before-require' is non-nil, this function performs the
compilation (if necessary) of the dependencies."
- (if coq-compile-before-require
- (let (;; coq-object-hash-symbol serves as a pointer to the
- ;; coq-obj-hash (see coq-seq-make-lib-up-to-date). The hash
- ;; will be initialized when needed and stored in the value
- ;; cell of coq-object-hash-symbol. The symbol is initialized
- ;; here to use one hash for all the requires that are added now.
- (coq-object-hash-symbol nil)
- string)
- (dolist (item queueitems)
- (let ((string (mapconcat 'identity (nth 1 item) " ")))
- (when (and string
- (string-match coq-require-command-regexp string))
- (let ((span (car item))
- (start (match-end 0))
- (prefix (match-string 1 string)))
- (span-add-delete-action
- span
- `(lambda ()
- (coq-unlock-all-ancestors-of-span ,span)))
- (coq-compile-save-some-buffers)
- ;; now process all required modules
- (while (string-match coq-require-id-regexp string start)
- (setq start (match-end 0))
- (coq-seq-check-module 'coq-object-hash-symbol span
- (match-string 1 string) prefix)))))))))
+ (when coq-compile-before-require
+ (defvar coq-object-hash-symbol)
+ (let (;; coq-object-hash-symbol serves as a pointer to the
+ ;; coq-obj-hash (see coq-seq-make-lib-up-to-date). The hash
+ ;; will be initialized when needed and stored in the value
+ ;; cell of coq-object-hash-symbol. The symbol is initialized
+ ;; here to use one hash for all the requires that are added now.
+ ;; FIXME: Why not create the hash table eagerly here and
+ ;; avoid the indirection (and avoid passing dynbound variable
+ ;; names around)?
+ (coq-object-hash-symbol nil))
+ (dolist (item queueitems)
+ (let ((string (mapconcat 'identity (nth 1 item) " ")))
+ (when (and string
+ (string-match coq-require-command-regexp string))
+ (let ((span (car item))
+ (start (match-end 0))
+ (prefix (match-string 1 string)))
+ (span-add-delete-action
+ span
+ (lambda () (coq-unlock-all-ancestors-of-span span)))
+ (coq-compile-save-some-buffers)
+ ;; now process all required modules
+ (while (string-match coq-require-id-regexp string start)
+ (setq start (match-end 0))
+ (coq-seq-check-module 'coq-object-hash-symbol span
+ (match-string 1 string) prefix)))))))))
(provide 'coq-seq-compile)
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 39c6842..2c3b577 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -87,7 +87,7 @@ indentation work well.
An example of cofiguration is:
-(setq coq-smie-user-tokens '((\"xor\" . \"or\") (\"ifb\" . \"if\")))
+ (setq coq-smie-user-tokens '((\"xor\" . \"or\") (\"ifb\" . \"if\")))
to have token \"xor\" and \"ifb\" be considered as having
repectively same priority and associativity as \"or\" and \"if\".
@@ -158,7 +158,7 @@ attention to case differences."
;; coq grammar tacticals. This is not too problematic here since only
;; in records the indentation changes (maily for ";").
(defun coq-smie-is-tactic ()
- (let* ((pos (point))
+ (let* (;; (pos (point))
(cmdstrt (save-excursion (coq-find-real-start)))
(enclosing (coq-is-inside-enclosing cmdstrt)))
(cond
@@ -361,12 +361,11 @@ inside parenthesis)."
(let ((parops ; corresponding matcher may be a list
(if (listp (car parop)) (car parop) (cons (car parop)
nil))))
; go to corresponding closer or meet "."
- (when (member
- (coq-smie-search-token-backward
- (append parops (cons "." nil))
- end ignore-between)
- (cons "." nil))
- next))
+ (coq-smie-search-token-backward
+ ;; Add "." at the head of the list, since
+ ;; it's more efficient and ordering is ignored anyway.
+ (cons "." parops)
+ end ignore-between))
;; Do not consider "." when not followed by a space
;(message "SPACE?: %S , %S , %S" next next (looking-at
".[[:space:]]"))
(when (or (not (equal next "."))
@@ -558,7 +557,7 @@ The point should be at the beginning of the command name."
;; with" is for mutual definitions where both sides are of the same
;; level
(defun coq-smie-:=-deambiguate ()
- (let* ((orig (point))
+ (let* (;; (orig (point))
(cmdstrt (save-excursion (coq-find-real-start)))
(corresp (coq-smie-search-token-backward
'("let" "Inductive" "CoInductive" "{|" "." "with" "Module"
"where"
@@ -592,7 +591,7 @@ The point should be at the beginning of the command name."
(defun coq-smie-semicolon-deambiguate ()
- (let* ((pos (point))
+ (let* (;; (pos (point))
(cmdstrt (save-excursion (coq-find-real-start)))
(istac (or (coq-smie-is-tactic)
(coq-smie-is-ltacdef)
@@ -834,9 +833,12 @@ The point should be at the beginning of the command name."
(let ((prev-interesting
(coq-smie-search-token-backward
'("let" "match" "lazymatch" "multimatch" "lazy_match"
"mult_match" ;"eval" should be "eval in" but this is not supported by
search-token-backward
- "." ) nil
- '((("match" "lazymatch" "multimatch" "lazy_match" "mult_match")
. "with") (("let" ;"eval"
- ) . "in")))))
+ "." )
+ nil
+ '((("match" "lazymatch" "multimatch" "lazy_match" "mult_match")
+ . "with")
+ (("let") ;"eval"
+ . "in")))))
(cond
((member prev-interesting '("." nil)) "in tactic")
((equal prev-interesting "let") "in let")
@@ -1153,9 +1155,8 @@ If nil, default to `proof-indent' if it exists or to
`smie-indent-basic'."
(let* ((beg (if (listp (car parent)) (caar parent) (car parent)))
(end (cadr parent))
(regi (list (list beg end)))
- (tok (caddr parent))
+ ;; (tok (caddr parent))
(face (cond
- ((equal num 1) 'hlt-regexp-level-1)
((equal num 2) 'hlt-regexp-level-2)
(t 'hlt-regexp-level-1))))
(and parent (hlt-highlight-regions regi face)))))
@@ -1281,7 +1282,7 @@ KIND is the situation and TOKEN is the thing w.r.t which
the rule applies."
;; (if (smie-rule-bolp) 2 0))
;(and (zerop (length tok)) (member (char-before) '(?\{ ?\})))
((and (zerop (length token))
- (looking-back "}") ;; "|}" useless when looking backward
+ (looking-back "}" (1- (point))) ;; "|}" useless when looking
backward
(not coq-indent-box-style))
(smie-backward-sexp)
(smie-backward-sexp t)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index 4c2375c..b8571d2 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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -590,8 +590,8 @@ so for the following reasons:
("Test" nil "Test" nil "Test" nil t) ; let us not highlight all possible
options for Test
("Timeout" nil "Timeout" nil "Timeout")
)
- "Coq queries command, that deserve a separate menu for sending them to coq
without insertion."
- )
+ "Coq queries command.
+They deserve a separate menu for sending them to Coq without insertion.")
;; command that are not declarations, definition or goal starters
(defvar coq-other-commands-db
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 804831d..48ddf77 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -137,13 +137,11 @@ Interactively (with INTERACTIVE-P), show that number."
(when interactive-p (coq-show-version))
coq-autodetected-version)
-(defun coq-autodetect-help (&optional interactive-p)
- "Record the output of coqotp -help in `coq-autodetected-help'."
+(defun coq-autodetect-help (&optional _interactive-p)
+ "Record the output of coqtop -help in `coq-autodetected-help'."
(interactive '(t))
(let ((coq-output (coq-callcoq "-help")))
- (if coq-output
- (setq coq-autodetected-help coq-output)
- (setq coq-autodetected-help ""))))
+ (setq coq-autodetected-help (or coq-output ""))))
(defun coq--version< (v1 v2)
@@ -654,7 +652,7 @@ Does nothing if `coq-use-project-file' is nil."
(add-hook 'coq-mode-hook
(lambda ()
(add-hook 'hack-local-variables-hook
- 'coq-load-project-file
+ #'coq-load-project-file
nil t)))
; detecting coqtop args should happen at the last moment before
@@ -672,7 +670,7 @@ Does nothing if `coq-use-project-file' is nil."
(lambda ()
(when (and (fboundp 'show-paren--default)
(boundp 'show-paren-data-function))
- (setq show-paren-data-function 'show-paren--default))))
+ (setq show-paren-data-function #'show-paren--default))))
diff --git a/coq/coq-unicode-tokens.el b/coq/coq-unicode-tokens.el
index 349038c..c4a26b7 100644
--- a/coq/coq-unicode-tokens.el
+++ b/coq/coq-unicode-tokens.el
@@ -1,9 +1,9 @@
-;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*-
coding: utf-8; -*-
+;;; coq-unicode-tokens.el --- (No) Tokens for Unicode Tokens package -*-
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-2021 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,7 +169,7 @@ The string mapping can be anything, but should be such that
tokens can be uniquely recovered from a decoded text; otherwise
results will be undefined when files are saved."
:type 'unicode-tokens-token-symbol-map
- :set 'coq-unicode-tokens-set
+ :set #'coq-unicode-tokens-set
:group 'coq
:tag "Coq Unicode Token Mapping")
@@ -253,7 +253,7 @@ performed. This means that the target strings need to have
a defined
meaning to be useful."
:type '(repeat (cons (string :tag "Shortcut sequence")
(string :tag "Unicode string")))
- :set 'coq-unicode-tokens-set
+ :set #'coq-unicode-tokens-set
:group 'coq
:tag "Coq Unicode Input Shortcuts")
@@ -275,7 +275,7 @@ meaning to be useful."
("Superscript" "^^" sup)))
;(defconst coq-control-region-format-regexp
"\\(\s*%s\{\\)\\([^}]*\\)\\(\}\s*\\)")
-(defconst coq-control-region-format-regexp "\\(%s\{\\)\\([^}]*\\)\\(\}\\)")
+(defconst coq-control-region-format-regexp "\\(%s{\\)\\([^}]*\\)\\(}\\)")
(defconst coq-control-regions
'(("Subscript" "," "" sub)
diff --git a/coq/coq.el b/coq/coq.el
index 1f59934..20238da 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -1,9 +1,9 @@
-;;; coq.el --- Major mode for Coq proof assistant -*- coding: utf-8 -*-
+;;; coq.el --- Major mode for Coq proof assistant -*- 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-2018 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2021 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
@@ -381,7 +381,7 @@ that should maybe not be classified as urgent messages.")
"Find forward the next really urgent message.
Return the position of the beginning of the message (after the
annotation-start) if found."
- (let ((again t) (found nil) (start-start nil) (end-end nil)
+ (let ((again t) (start-start nil) (end-end nil) ;; (found nil)
(eager proof-shell-eager-annotation-start))
(while again
(setq start-start (and (re-search-forward eager nil 'limit)
@@ -458,14 +458,12 @@ This is a subroutine of `proof-shell-filter'."
(min end
(save-excursion (end-of-line) (point))
(+ start 75))))
- (let*
- ((face
- (progn (goto-char start)
- (if (looking-at "<infomsg>") 'default
- 'proof-eager-annotation-face)))
- (str (proof-shell-strip-eager-annotations start end))
- (strnotrailingspace
- (coq-remove-starting-blanks (coq-remove-trailing-blanks str))))
+ (goto-char start)
+ (let* (;; (face (if (looking-at "<infomsg>") 'default
+ ;; 'proof-eager-annotation-face))
+ (str (proof-shell-strip-eager-annotations start end))
+ (strnotrailingspace
+ (coq-remove-starting-blanks (coq-remove-trailing-blanks str))))
(pg-response-display-with-face strnotrailingspace))) ; face
@@ -708,7 +706,7 @@ If locked span already has a state number, then do nothing.
Also updates
;; processed externally (i.e. Require, etc), nothing to do
;; (should really be unlocked when we undo the Require).
nil
- (let* ((naborts 0)
+ (let* (;; (naborts 0)
(proofdepth (coq-get-span-proofnum span))
(proofstack (coq-get-span-proofstack span))
(span-staten (coq-get-span-statenum span))
@@ -732,7 +730,7 @@ If locked span already has a state number, then do nothing.
Also updates
(cons 'goal (int-to-string coq-current-goal)))
((looking-at "\\(?:sub\\)?goal \\([0-9]+\\) is:\n")
(goto-char (match-end 0))
- (cons 'goal (match-string 1)) ;FIXME: This is dead-code!? --Stef
+ ;; (cons 'goal (match-string 1)) ;FIXME: This is dead-code!? --Stef
(setq coq-current-goal (string-to-number (match-string 1))))
((proof-looking-at proof-shell-assumption-regexp)
(cons 'hyp (match-string 1)))
@@ -787,15 +785,13 @@ the *goals* buffer."
(completing-read "Infos on notation (TAB to see list): "
notation-print-kinds-table))
(s (read-string "Name (empty for all): "))
- (all (string-equal s "")))
+ ;; (all (string-equal s ""))
+ )
(cond
((and (string-equal mods "Print Scope(s)") (string-equal s ""))
(proof-shell-invisible-command (format "Print Scopes.")))
(t
- (proof-shell-invisible-command (format "%s %s ." mods s)))
- )
- )
- )
+ (proof-shell-invisible-command (format "%s %s ." mods s))))))
(defun coq-remove-trailing-dot (s)
"Return the string S without its trailing \".\" if any.
@@ -955,11 +951,13 @@ the time of writing this documentation)."
'waitforit nil 'no-response-display
'empty-action-list))))
(defun coq-ask-do-set-unset (ask do setcmd unsetcmd
- &optional dontguess postformatcmd tescmd)
+ &optional dontguess postformatcmd _tescmd)
"Ask for an ident id and execute command DO in SETCMD mode.
More precisely it executes SETCMD, then DO id and finally silently
UNSETCMD. See `coq-command-with-set-unset'."
- (let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd
tescmd)))
+ (let* ((cmd)
+ ;; (postform (if (eq postformatcmd nil) 'identity postformatcmd
tescmd))
+ )
(proof-shell-ready-prover)
(setq cmd (coq-guess-or-ask-for-string ask dontguess))
(coq-command-with-set-unset setcmd (concat do " " cmd) unsetcmd
postformatcmd)))
@@ -1186,9 +1184,9 @@ Printing All set."
;; FIXME: hopefully this will eventually become a non synchronized option and
;; we can remove this.
-(defun coq-set-auto-adapt-printing-width (&optional symb val); args are for
:set compatibility
+(defun coq-set-auto-adapt-printing-width (&optional _symb val); args are for
:set compatibility
"Function called when setting `auto-adapt-printing-width'."
- (setq symb val) ;; FIXME this is wrong (it should be 'set', but it would set
nil sometimes)
+ (setq coq-auto-adapt-printing-width val)
(if coq-auto-adapt-printing-width
(progn
(add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
@@ -1196,6 +1194,15 @@ Printing All set."
(remove-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
(remove-hook 'proof-retract-command-hook #'coq-reset-printing-width)))
+(defun coq--show-proof-stepwise-cmds ()
+ (when coq-show-proof-stepwise
+ (if (coq--post-v811)
+ (pcase coq-diffs
+ ('off '("Show Proof."))
+ ('on '("Show Proof Diffs."))
+ ('removed '("Show Proof Diffs removed.")))
+ '("Show Proof."))))
+
;; In case of nested proofs (which are announced as obsolete in future versions
;; of coq) Coq does not show the goals of enclosing proof when closing a nested
;; proof. This is coq's proof-shell-empty-action-list-command function which
@@ -1218,34 +1225,17 @@ should match the `coq-show-proof-diffs-regexp'."
;; If user issued a printing option then t printing.
(and (string-match-p "\\(S\\|Uns\\)et\\s-+Printing" cmd)
(> (length coq-last-but-one-proofstack) 0)))
- (let ((showlist (list "Show.")))
- (when coq-show-proof-stepwise
- (add-to-list 'showlist
- (if (coq--post-v811)
- (or
- (when (eq coq-diffs 'off) "Show Proof.")
- (when (eq coq-diffs 'on) "Show Proof Diffs.")
- (when (eq coq-diffs 'removed) "Show Proof Diffs
removed."))
- "Show Proof.")
- t))
- showlist))
+ `("Show."
+ . ,(coq--show-proof-stepwise-cmds)))
((or
;; If we go back in the buffer and the number of abort is less than
;; the number of nested goals, then Unset Silent and Show the goal
(and (string-match-p "BackTo\\s-" cmd)
(> (length coq-last-but-one-proofstack) coq--retract-naborts)))
- (let ((showlist (list "Unset Silent." (if (coq--post-v810) (coq-diffs)
"Show."))))
- (when coq-show-proof-stepwise
- (add-to-list 'showlist
- (if (coq--post-v811)
- (or
- (when (eq coq-diffs 'off) "Show Proof.")
- (when (eq coq-diffs 'on) "Show Proof Diffs." )
- (when (eq coq-diffs 'removed) "Show Proof Diffs
removed."))
- "Show Proof.")
- t))
- showlist))
+ `("Unset Silent."
+ ,(if (coq--post-v810) (coq-diffs) "Show.")
+ . ,(coq--show-proof-stepwise-cmds)))
((or
;; If we go back in the buffer and not in the above case, then only Unset
@@ -1260,13 +1250,7 @@ should match the `coq-show-proof-diffs-regexp'."
;; If doing (not closing) a proof, Show Proof if need be
(and (not (string-match-p coq-save-command-regexp-strict cmd))
(> (length coq-last-but-one-proofstack) 0)))
- (when coq-show-proof-stepwise
- (if (coq--post-v811)
- (or
- (when (eq coq-diffs 'off) (list "Show Proof." ))
- (when (eq coq-diffs 'on) (list "Show Proof Diffs."))
- (when (eq coq-diffs 'removed) (list "Show Proof Diffs removed.")))
- (list "Show Proof."))))))
+ (coq--show-proof-stepwise-cmds))))
(defpacustom auto-adapt-printing-width t
@@ -1304,11 +1288,11 @@ necessary.")
"Return the width of a window currently displaying BUFFER."
(let*
((buf-wins (get-buffer-window-list buffer nil t))
- (dummy (if (not (eq 1 (length buf-wins)))
- (display-warning
- 'proof-general
- "Zero or more than one goals window, guessing window width."
- :debug)))
+ (_ (if (not (eq 1 (length buf-wins)))
+ (display-warning
+ 'proof-general
+ "Zero or more than one goals window, guessing window width."
+ :debug)))
(buf-win (car buf-wins)));; TODO return the widest one instead of the
first?
;; return nil if no goal buffer found
(and buf-win (window-width buf-win))))
@@ -1323,7 +1307,7 @@ necessary.")
"Return the probable width of goals buffer if it pops up now.
This is a guess based on the current width of goals buffer if
present, current pg display mode and current geometry otherwise."
- (let (pol (proof-guess-3win-display-policy proof-three-window-mode-policy))
+ (let ((pol (proof-guess-3win-display-policy proof-three-window-mode-policy)))
(cond
;; goals buffer is visible, bingo
((coq-goals-window-width))
@@ -1360,7 +1344,7 @@ redisplayed."
(when (and show (not (null (cl-caddr (coq-last-prompt-info-safe)))))
(proof-shell-invisible-command (format "Show.") t nil
'no-error-display)))))
-(defun coq-adapt-printing-width-and-show(&optional show width)
+(defun coq-adapt-printing-width-and-show (&optional _show width)
(interactive)
(coq-adapt-printing-width t width))
@@ -1664,7 +1648,8 @@ See `coq-highlight-hyp'."
(insert hyp-name)))
;;;;;;;;;;; Hiding Hypothesis ;;;;;;;;;;;
-(defvar coq-hidden-hyp-map (make-sparse-keymap) "Keymap for hidden
hypothesis.")
+(defvar coq-hidden-hyp-map (make-sparse-keymap)
+ "Keymap for hidden hypothesis.")
(defvar coq-hidden-hyps nil
"List of hypothesis that should be hidden in goals buffer.
@@ -1710,14 +1695,15 @@ Used on hyptohesis overlays in goals buffer mainly."
(overlay-put hyp-overlay 'keymap coq-hidden-hyp-map)
(overlay-put hypcross-ov 'display (coq-hypcross-folded-string)))))
-(defun coq-configure-hyp-overlay-visible (hyp-overlay h)
+(defun coq-configure-hyp-overlay-visible (hyp-overlay _h)
(when hyp-overlay
(overlay-put hyp-overlay 'display nil)
(overlay-put hyp-overlay 'evaporate t)
(overlay-put hyp-overlay 'mouse-face nil)
(overlay-put hyp-overlay 'help-echo nil)
(overlay-put hyp-overlay 'keymap nil)
- (overlay-put (overlay-get hyp-overlay 'hypcross-ov) 'display
(coq-hypcross-unfolded-string))))
+ (overlay-put (overlay-get hyp-overlay 'hypcross-ov)
+ 'display (coq-hypcross-unfolded-string))))
(defun coq-fold-hyp-aux (h)
"Fold hypothesis H's type from the context temporarily.
@@ -1913,7 +1899,7 @@ at `proof-assistant-settings-cmds' evaluation time.")
(setq proof-terminal-string ".")
;; superseded by coq-script-parse-function
;;(setq proof-script-command-end-regexp coq-script-command-end-regexp)
- (setq proof-script-parse-function 'coq-script-parse-function)
+ (setq proof-script-parse-function #'coq-script-parse-function)
(setq proof-script-comment-start comment-start)
(setq proof-script-comment-end comment-end)
(setq proof-script-insert-newlines nil)
@@ -2164,7 +2150,7 @@ Set Diffs setting if Coq is running and has a version >=
8.10."
(const :tag "Show diffs: only added" on)
(const :tag "Show diffs: added and removed" removed))
:safe (lambda (v) (member v '(off on removed)))
- :set 'coq-diffs--setter
+ :set #'coq-diffs--setter
:group 'coq)
;; Obsolete:
@@ -2287,14 +2273,13 @@ The not yet delayed output is in the region
(let ((subgoal-id (match-string-no-properties 1)))
(unless (gethash subgoal-id proof-tree-sequent-hash)
;; (message "CPTGNS new sequent %s found" subgoal-id)
- (setq proof-action-list
- (cons (proof-shell-action-list-item
- (coq-show-sequent-command subgoal-id)
- (proof-tree-make-show-goal-callback (car
proof-info))
- '(no-goals-display
- no-response-display
- proof-tree-show-subgoal))
- proof-action-list))))))))))
+ (push (proof-shell-action-list-item
+ (coq-show-sequent-command subgoal-id)
+ (proof-tree-make-show-goal-callback (car proof-info))
+ '(no-goals-display
+ no-response-display
+ proof-tree-show-subgoal))
+ proof-action-list)))))))))
(add-hook 'proof-tree-urgent-action-hook #'coq-proof-tree-get-new-subgoals)
@@ -2344,7 +2329,7 @@ This is the Coq incarnation of
`proof-tree-find-undo-position'."
(defvar coq--proof-tree-must-disable-evars nil
"Remember if evar printing must be disabled when leaving the current proof.")
-(defun coq-proof-tree-enable-evar-callback (span)
+(defun coq-proof-tree-enable-evar-callback (_span)
"Callback for the evar printing status test.
This is the callback for the command ``Test Printing Dependent Evars Line''.
It checks whether evar printing was off and remembers that
@@ -2465,6 +2450,9 @@ This is a hook setting for `pg-after-fontify-output-hook'
to
enable identifiers to be highlighted and allow useful
mouse activation."
(goto-char (point-min))
+ ;; FIXME: This regexp is obviously wrong. The backslashes have no effect
+ ;; (for lack of being doubled), so Emacs searches for "(w+[^w])" :-(
+ ;; Also the \w regexp operator cannot be used within a [...] char range.
(while (re-search-forward "\(\w+[^\w]\)" nil t)
(replace-match "\372\200\373\\1\374" nil t)))
@@ -2473,7 +2461,7 @@ mouse activation."
;; Context-senstive in-span menu additions
;;
-(defun coq-create-span-menu (span idiom name)
+(defun coq-create-span-menu (span idiom _name)
(if (eq idiom 'proof)
(let ((thm (span-property span 'name)))
(list (vector
@@ -2659,7 +2647,7 @@ Warning: this makes the error messages (and location)
wrong.")
;; itself sets the 'dependencies property of the span, and calls
;; `proof-dependencies-system-specific'. The latter is bound to
;; `coq-dependencies-system-specific' below.
-(setq coq-shell-theorem-dependency-list-regexp
+(defconst coq-shell-theorem-dependency-list-regexp
"<infomsg>\n?The proof of \\(?1:[^ \n]+\\)\\(?: \\|\n\\)should start with
one of the following commands:\\(?: \\|\n\\)Proof using\\(?2:[^.]*\\)\\.")
(defcustom coq-accept-proof-using-suggestion 'highlight
@@ -2712,12 +2700,12 @@ Remarks and limitations:
(let* ((deps (span-property-safe span 'dependencies))
(specialspans (spans-at-region-prop (span-start span) (span-end
span) 'proofusing))
(specialspan (and specialspans (not (cdr specialspans)) (car
specialspans)))
- (suggested (mapconcat 'identity deps " "))
+ (suggested (mapconcat #'identity deps " "))
(suggested (coq-hack-proofusing-suggestion suggested))
(name (concat " insert \"proof using " suggested "\""))
- (fn `(lambda (sp)
+ (fn (lambda (sp)
(coq-insert-proof-using-suggestion sp t)
- (and ,specialspan (span-delete ,specialspan)))))
+ (and specialspan (span-delete specialspan)))))
(list "-------------" (vector name `(,fn ,span) t))))
"Coq specific additional menu entry for \"Proof using\".
annotation. See `proof-dependency-menu-system-specific'." )
@@ -2734,7 +2722,7 @@ insertion point for the \"using\" annotation. ")
;; span is typically the whole theorem statement+proof span built after a save
;; command
-(defun coq-highlight-span-dependencies (span suggested)
+(defun coq-highlight-span-dependencies (span _suggested)
(goto-char (span-start span))
; Search for the "Proof" command and build a hilighted span on it
(let* ((endpos (re-search-forward coq-proof-using-regexp))
@@ -2744,7 +2732,7 @@ insertion point for the \"using\" annotation. ")
(span-set-property newspan 'help-echo "Right click to insert \"proof
using\"")
(span-set-property newspan 'proofusing t)))
-(defun coq-insert-proof-using (proof-pos previous-content insert-point
string-suggested)
+(defun coq-insert-proof-using (_proof-pos _previous-content insert-point
string-suggested)
(goto-char insert-point)
(let ((spl proof-locked-span))
(span-read-write spl) ; temporarily make the locked span writable
@@ -2754,7 +2742,7 @@ insertion point for the \"using\" annotation. ")
(defun coq-insert-suggested-dependency ()
(interactive)
(let* ((span (span-at (point) 'type))
- (deps (span-property-safe span 'dependencies))
+ ;; (deps (span-property-safe span 'dependencies))
(specialspans (spans-at-region-prop (span-start span) (span-end span)
'proofusing))
(specialspan (and specialspans (not (cdr specialspans)) (car
specialspans))))
(coq-insert-proof-using-suggestion span t)
@@ -2777,7 +2765,7 @@ SPAN is the span of the whole theorem (statement +
proof)."
(insert-point (match-beginning 1))
(previous-string (match-string 1))
(previous-content (split-string previous-string))
- (string-suggested (mapconcat 'identity suggested " "))
+ (string-suggested (mapconcat #'identity suggested " "))
(string-suggested (coq-hack-proofusing-suggestion
string-suggested))
;; disabled for now it never happens because Coq would
suggest anything?
(same (and nil previous-content
@@ -2808,7 +2796,7 @@ Used for automatic insertion of \"Proof using\"
annotations.")
(goto-char (proof-unprocessed-begin))
(coq-find-real-start)
(let* ((pt (point))
- (dummy (coq-script-parse-cmdend-forward))
+ (_ (coq-script-parse-cmdend-forward))
(cmd (buffer-substring pt (point)))
(newcmd (if (coq-tactic-already-has-an-as-close cmd)
nil
@@ -2932,34 +2920,34 @@ Completion is on a quasi-exhaustive list of Coq
tacticals."
;; Insertion commands
-(define-key coq-keymap [(control ?i)] 'coq-insert-intros)
-(define-key coq-keymap [(control ?m)] 'coq-insert-match)
-(define-key coq-keymap [(control ?\()] 'coq-insert-section-or-module)
-(define-key coq-keymap [(control ?\))] 'coq-end-Section)
-(define-key coq-keymap [(control ?t)] 'coq-insert-tactic)
-(define-key coq-keymap [?t] 'coq-insert-tactical)
-(define-key coq-keymap [?!] 'coq-insert-solve-tactic) ; will work in tty
-(define-key coq-keymap [(control ?\s)] 'coq-insert-term)
-(define-key coq-keymap [(control return)] 'coq-insert-command)
-(define-key coq-keymap [(control ?q)] 'coq-query)
-(define-key coq-keymap [(control ?r)] 'coq-insert-requires)
+(define-key coq-keymap [(control ?i)] #'coq-insert-intros)
+(define-key coq-keymap [(control ?m)] #'coq-insert-match)
+(define-key coq-keymap [(control ?\()] #'coq-insert-section-or-module)
+(define-key coq-keymap [(control ?\))] #'coq-end-Section)
+(define-key coq-keymap [(control ?t)] #'coq-insert-tactic)
+(define-key coq-keymap [?t] #'coq-insert-tactical)
+(define-key coq-keymap [?!] #'coq-insert-solve-tactic) ; will work
in tty
+(define-key coq-keymap [(control ?\s)] #'coq-insert-term)
+(define-key coq-keymap [(control return)] #'coq-insert-command)
+(define-key coq-keymap [(control ?q)] #'coq-query)
+(define-key coq-keymap [(control ?r)] #'coq-insert-requires)
; [ for "as [xxx]" is easy to remember, ccontrol-[ would be better but hard to
type on french keyboards
; anyway company-coq should provide an "as!<TAB>".
-(define-key coq-keymap [(?\[)] 'coq-insert-as-in-next-command) ;; not for
goal/response buffer?
+(define-key coq-keymap [(?\[)] #'coq-insert-as-in-next-command) ;; not
for goal/response buffer?
; Query commands
-(define-key coq-keymap [(control ?s)] 'coq-Show)
-(define-key coq-keymap [?r] 'proof-store-response-win)
-(define-key coq-keymap [?g] 'proof-store-goals-win)
-(define-key coq-keymap [(control ?o)] 'coq-SearchIsos)
-(define-key coq-keymap [(control ?p)] 'coq-Print)
-(define-key coq-keymap [(control ?b)] 'coq-About)
-(define-key coq-keymap [(control ?a)] 'coq-Search)
-(define-key coq-keymap [(control ?c)] 'coq-Check)
-(define-key coq-keymap [?h] 'coq-PrintHint)
-(define-key coq-keymap [(control ?l)] 'coq-LocateConstant)
-(define-key coq-keymap [(control ?n)] 'coq-LocateNotation)
-(define-key coq-keymap [(control ?w)] 'coq-ask-adapt-printing-width-and-show)
+(define-key coq-keymap [(control ?s)] #'coq-Show)
+(define-key coq-keymap [?r] #'proof-store-response-win)
+(define-key coq-keymap [?g] #'proof-store-goals-win)
+(define-key coq-keymap [(control ?o)] #'coq-SearchIsos)
+(define-key coq-keymap [(control ?p)] #'coq-Print)
+(define-key coq-keymap [(control ?b)] #'coq-About)
+(define-key coq-keymap [(control ?a)] #'coq-Search)
+(define-key coq-keymap [(control ?c)] #'coq-Check)
+(define-key coq-keymap [?h] #'coq-PrintHint)
+(define-key coq-keymap [(control ?l)] #'coq-LocateConstant)
+(define-key coq-keymap [(control ?n)] #'coq-LocateNotation)
+(define-key coq-keymap [(control ?w)] #'coq-ask-adapt-printing-width-and-show)
;(proof-eval-when-ready-for-assistant
; (define-key ??? [(control c) (control a)] (proof-ass keymap)))
@@ -2967,61 +2955,61 @@ Completion is on a quasi-exhaustive list of Coq
tacticals."
;(proof-eval-when-ready-for-assistant
; (define-key ??? [(control c) (control a)] (proof-ass keymap)))
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?c)]
'coq-Check)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)]
'coq-Print)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)]
'coq-SearchIsos)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)]
'coq-About)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)]
'coq-Search)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?s)]
'coq-Show)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)?r]
'proof-store-response-win)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)?g]
'proof-store-goals-win)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?q)]
'coq-query)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)]
'coq-ask-adapt-printing-width-and-show)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)]
'coq-LocateConstant)
-(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)]
'coq-LocateNotation)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?c)]
#'coq-Check)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?p)]
#'coq-Print)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?o)]
#'coq-SearchIsos)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?b)]
#'coq-About)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?a)]
#'coq-Search)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?s)]
#'coq-Show)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)?r]
#'proof-store-response-win)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)?g]
#'proof-store-goals-win)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)?h] #'coq-PrintHint)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?q)]
#'coq-query)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?w)]
#'coq-ask-adapt-printing-width-and-show)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?l)]
#'coq-LocateConstant)
+(define-key coq-goals-mode-map [(control ?c)(control ?a)(control ?n)]
#'coq-LocateNotation)
;; specific to goals buffer: (un)foldinng and (un)highlighting shortcuts
-(define-key coq-goals-mode-map [?f] 'coq-toggle-fold-hyp-at-point)
-(define-key coq-goals-mode-map [?F] 'coq-unfold-hyps)
-(define-key coq-goals-mode-map [?h] 'coq-toggle-highlight-hyp-at-point)
-(define-key coq-goals-mode-map [?H] 'coq-unhighlight-selected-hyps)
-
-
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)]
'coq-Check)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?p)]
'coq-Print)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?o)]
'coq-SearchIsos)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?b)]
'coq-About)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)]
'coq-Search)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?s)]
'coq-Show)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?r)]
'proof-store-response-win)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)]
'proof-store-goals-win)
-(define-key coq-response-mode-map [(control ?c)(control ?a)?h] 'coq-PrintHint)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?q)]
'coq-query)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?w)]
'coq-ask-adapt-printing-width-and-show)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?l)]
'coq-LocateConstant)
-(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?n)]
'coq-LocateNotation)
+(define-key coq-goals-mode-map [?f] #'coq-toggle-fold-hyp-at-point)
+(define-key coq-goals-mode-map [?F] #'coq-unfold-hyps)
+(define-key coq-goals-mode-map [?h] #'coq-toggle-highlight-hyp-at-point)
+(define-key coq-goals-mode-map [?H] #'coq-unhighlight-selected-hyps)
+
+
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?c)]
#'coq-Check)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?p)]
#'coq-Print)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?o)]
#'coq-SearchIsos)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?b)]
#'coq-About)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?a)]
#'coq-Search)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?s)]
#'coq-Show)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?r)]
#'proof-store-response-win)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?g)]
#'proof-store-goals-win)
+(define-key coq-response-mode-map [(control ?c)(control ?a)?h] #'coq-PrintHint)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?q)]
#'coq-query)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?w)]
#'coq-ask-adapt-printing-width-and-show)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?l)]
#'coq-LocateConstant)
+(define-key coq-response-mode-map [(control ?c)(control ?a)(control ?n)]
#'coq-LocateNotation)
(when coq-remap-mouse-1
- (define-key proof-mode-map [(control down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-mode-map [(shift down-mouse-1)] 'coq-id-under-mouse-query)
- (define-key proof-mode-map [(control mouse-1)] '(lambda () (interactive)))
- (define-key proof-mode-map [(shift mouse-1)] '(lambda () (interactive)))
- (define-key proof-mode-map [(control shift down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-mode-map [(control shift mouse-1)] '(lambda ()
(interactive)))
+ (define-key proof-mode-map [(control down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-mode-map [(shift down-mouse-1)] #'coq-id-under-mouse-query)
+ (define-key proof-mode-map [(control mouse-1)] #'ignore)
+ (define-key proof-mode-map [(shift mouse-1)] #'ignore)
+ (define-key proof-mode-map [(control shift down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-mode-map [(control shift mouse-1)] #'ignore)
- (define-key proof-response-mode-map [(control down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-response-mode-map [(shift down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-response-mode-map [(control mouse-1)] '(lambda ()
(interactive)))
- (define-key proof-response-mode-map [(shift mouse-1)] '(lambda ()
(interactive)))
- (define-key proof-response-mode-map [(control shift down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-response-mode-map [(control shift mouse-1)] '(lambda ()
(interactive)))
+ (define-key proof-response-mode-map [(control down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-response-mode-map [(shift down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-response-mode-map [(control mouse-1)] #'ignore)
+ (define-key proof-response-mode-map [(shift mouse-1)] #'ignore)
+ (define-key proof-response-mode-map [(control shift down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-response-mode-map [(control shift mouse-1)] #'ignore)
- (define-key proof-goals-mode-map [(control down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-goals-mode-map [(shift down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-goals-mode-map [(control mouse-1)] '(lambda ()
(interactive)))
- (define-key proof-goals-mode-map [(shift mouse-1)] '(lambda ()
(interactive)))
- (define-key proof-goals-mode-map [(control shift down-mouse-1)]
'coq-id-under-mouse-query)
- (define-key proof-goals-mode-map [(control shift mouse-1)] '(lambda ()
(interactive))))
+ (define-key proof-goals-mode-map [(control down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-goals-mode-map [(shift down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-goals-mode-map [(control mouse-1)] #'ignore)
+ (define-key proof-goals-mode-map [(shift mouse-1)] #'ignore)
+ (define-key proof-goals-mode-map [(control shift down-mouse-1)]
#'coq-id-under-mouse-query)
+ (define-key proof-goals-mode-map [(control shift mouse-1)] #'ignore))
@@ -3029,22 +3017,22 @@ Completion is on a quasi-exhaustive list of Coq
tacticals."
;; button 3 folds it. Click on it with button 2 copies the names at current
;; point.
(when coq-hypname-map
- (define-key coq-hypname-map [(mouse-3)] 'coq-toggle-fold-hyp-at-mouse)
- (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point)
- (define-key coq-hypname-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
+ (define-key coq-hypname-map [(mouse-3)] #'coq-toggle-fold-hyp-at-mouse)
+ (define-key coq-hypcross-map [(return)] #'coq-toggle-fold-hyp-at-point)
+ (define-key coq-hypname-map [(mouse-2)] #'coq-insert-at-point-hyp-at-mouse))
;; Default binding: clicking on the cross to folds/unfold hyp.
;; Click on it with button 2 copies the names at current point.
(when coq-hypname-map
- (define-key coq-hypcross-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse)
- (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point)
- (define-key coq-hypcross-map [(mouse-2)] 'coq-insert-at-point-hyp-at-mouse))
+ (define-key coq-hypcross-map [(mouse-1)] #'coq-toggle-fold-hyp-at-mouse)
+ (define-key coq-hypcross-map [(return)] #'coq-toggle-fold-hyp-at-point)
+ (define-key coq-hypcross-map [(mouse-2)] #'coq-insert-at-point-hyp-at-mouse))
;; Ddefault binding: clicking on a hidden hyp with button 3 unfolds it, with
;; button 2 it copies hyp name at current point.
(when coq-hidden-hyp-map
- (define-key coq-hidden-hyp-map [(mouse-1)] 'coq-toggle-fold-hyp-at-mouse)
- (define-key coq-hypcross-map [(return)] 'coq-toggle-fold-hyp-at-point)
- (define-key coq-hidden-hyp-map [(mouse-2)]
'coq-insert-at-point-hyp-at-mouse))
+ (define-key coq-hidden-hyp-map [(mouse-1)] #'coq-toggle-fold-hyp-at-mouse)
+ (define-key coq-hypcross-map [(return)] #'coq-toggle-fold-hyp-at-point)
+ (define-key coq-hidden-hyp-map [(mouse-2)]
#'coq-insert-at-point-hyp-at-mouse))
;;;;;;;;;;;;;;;;;;;;;;;;
;; error handling
@@ -3258,7 +3246,7 @@ number of hypothesis displayed, without hiding the goal"
-(defun is-not-split-vertic (selected-window)
+(defun is-not-split-vertic (_selected-window)
(<= (- (frame-height) (window-height)) 2))
;; bug fixed in generic ocde, useless now:
@@ -3334,7 +3322,7 @@ this variable is not nil, then 1) it means that electric
terminator is off and 2) a double hit on the terminator act as
the usual electric terminator. See `proof-electric-terminator'."
:type 'boolean
- :set 'proof-set-value
+ :set #'proof-set-value
:group 'proof-user-options)
@@ -3414,7 +3402,7 @@ Starts a timer for a double hit otherwise."
(setq coq-double-hit-hot t)
(setq coq-double-hit-timer
(run-with-timer coq-double-hit-delay
- nil 'coq-unset-double-hit-hot))))
+ nil #'coq-unset-double-hit-hot))))
(defun coq-terminator-insert (&optional count)
"A wrapper on `proof-electric-terminator'.