diff --git a/Makefile b/Makefile
index b9b28aab5..739affe70 100644
--- a/Makefile
+++ b/Makefile
@@ -143,6 +143,14 @@ check-doc-magic:
+$(MAKE) -C doc magic
git diff --exit-code -- doc
+##
+## checkdoc : check the docstrings using the Emacs builtin checkdoc utility
+##
+.PHONY: checkdoc
+checkdoc: $(EL)
+ @$(EMACS) -Q --batch -l resources/checkdoc-config.el \
+ $(foreach file,$^,"--eval=(checkdoc-file \"$(file)\")")
+
##
## Make an individual .elc. Building separately means we need to be
## careful to add proper requires in source files and prevent
diff --git a/ci/compile-tests/001-mini-project/runtest.el b/ci/compile-tests/001-mini-project/runtest.el
index 6ebd31451..569719148 100644
--- a/ci/compile-tests/001-mini-project/runtest.el
+++ b/ci/compile-tests/001-mini-project/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -24,6 +26,7 @@
;; / \ / \
;; d e f
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -42,3 +45,7 @@
(cct-check-locked 24 'locked)
(cct-locked-ancestors 22 '("./b.v" "./d.v" "./e.v"))
(cct-locked-ancestors 23 '("./c.v" "./f.v")))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/002-require-no-dependencies/runtest.el b/ci/compile-tests/002-require-no-dependencies/runtest.el
index 0ea01fb62..b1db75ea5 100644
--- a/ci/compile-tests/002-require-no-dependencies/runtest.el
+++ b/ci/compile-tests/002-require-no-dependencies/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -21,6 +23,7 @@
;; |
;; c
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -46,3 +49,7 @@
(cct-check-locked 24 'locked)
(cct-locked-ancestors 22 '())
(cct-locked-ancestors 23 '("./c.v")))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/003-require-error/runtest.el b/ci/compile-tests/003-require-error/runtest.el
index 4c4d558c1..2ad883879 100644
--- a/ci/compile-tests/003-require-error/runtest.el
+++ b/ci/compile-tests/003-require-error/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -24,6 +26,7 @@
;;
;; and where a1, a2 and a3 are the 3 require commands in file a.v
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -43,3 +46,7 @@
(cct-check-locked 23 'unlocked)
(cct-file-newer "b.vo" test-start-time)
(cct-file-newer "c.vo" test-start-time)))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/004-dependency-cycle/runtest.el b/ci/compile-tests/004-dependency-cycle/runtest.el
index 143cf7a24..b47025735 100644
--- a/ci/compile-tests/004-dependency-cycle/runtest.el
+++ b/ci/compile-tests/004-dependency-cycle/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -24,6 +26,7 @@
;;
;; where a1 and a2 are the 2 require commands in file a.v.
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -59,3 +62,7 @@
(cct-check-locked 21 'locked)
(cct-check-locked 22 'unlocked)))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/005-change-recompile/runtest.el b/ci/compile-tests/005-change-recompile/runtest.el
index 2110fd5a2..7e98aa335 100644
--- a/ci/compile-tests/005-change-recompile/runtest.el
+++ b/ci/compile-tests/005-change-recompile/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -35,6 +37,8 @@
;;
;;
+;;; Code:
+
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -197,3 +201,7 @@ See `cct-generic-check-main-buffer'."
(check-main-buffer vo-times "71" '("./b.vo" "./d.vo" "./g.vo")
other-locked-files)
))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/006-ready-dependee/runtest.el b/ci/compile-tests/006-ready-dependee/runtest.el
index 7e96bb32b..f11b8dab7 100644
--- a/ci/compile-tests/006-ready-dependee/runtest.el
+++ b/ci/compile-tests/006-ready-dependee/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2020 Hendrik Tews
;;
@@ -27,12 +29,13 @@
;;
;; The idea is that the coqdep chain from b to j takes so long, that k
;; has been compiled and is in state ready before the coqdep results
-;; from j are processed. This works - unless the disk cache is cold.
-;; If it works the test triggers two bugs. First, k is locked with the
+;; from j are processed. This works - unless the disk cache is cold.
+;; If it works the test triggers two bugs. First, k is locked with the
;; require command of c. Second, the modification time of k is not
;; propagated to j, such that the whole chain from j to b is not
;; recompiled after k has changed.
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -59,7 +62,7 @@
(defun cct-replace-last-word (line word)
"Replace last word in line LINE with WORD.
In current buffer, go to the end of line LINE and one word
-backward. Replace the word there with WORD."
+backward. Replace the word there with WORD."
(cct-goto-line line)
(end-of-line)
(backward-word)
@@ -130,3 +133,7 @@ Combine all the following tests in this order:
"./h.vo" "./i.vo" "./j.vo" "./k.vo")
other-locked-files)
))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el
index 6696aa1bc..9d7ee38bf 100644
--- a/ci/compile-tests/007-slow-require/runtest.el
+++ b/ci/compile-tests/007-slow-require/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
;;
@@ -14,11 +16,11 @@
;;
;; Test two require jobs with different delays such that
;; coq-par-retire-top-level-job happens when the other require job is
-;; in each possible state. For specifying the different delays there
-;; are 6 mini projects, one for each test in this file. Each project
+;; in each possible state. For specifying the different delays there
+;; are 6 mini projects, one for each test in this file. Each project
;; consists of four files, a1.v, b1.v, c1.v and d1.v for the first one
-;; and a6.v, b6.v, c6.v and d6.v for the sixth one. Each project is
-;; one ert test, described further below. In each project or test, the
+;; and a6.v, b6.v, c6.v and d6.v for the sixth one. Each project is
+;; one ert test, described further below. In each project or test, the
;; top level require commands are asserted and retracted several times
;; with changes in different files to test (almost) all possible
;; internal state combinations.
@@ -53,12 +55,14 @@
;; seconds, such that the dependency link d->c is created when d is in
;; state enqueued-coqc.
+;;; Code:
+
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
;;; set configuration
(cct-configure-proof-general)
-(configure-delayed-coq)
+(configure-delayed-coq)
(defconst pre-b-ancestors '("./b" "./d")
"Ancestors of b without suffixes.")
@@ -213,3 +217,7 @@ XXX Test a setting where the second require job is still in state
(ert-deftest cct-slow-require-4 () (test-slow-require 4))
(ert-deftest cct-slow-require-5 () (test-slow-require 5))
(ert-deftest cct-slow-require-6 () (test-slow-require 6))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/008-default-dir/runtest.el b/ci/compile-tests/008-default-dir/runtest.el
index 42bf61a4e..a671ee189 100644
--- a/ci/compile-tests/008-default-dir/runtest.el
+++ b/ci/compile-tests/008-default-dir/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
;;
@@ -29,13 +31,14 @@
;; c
;;
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
;;; set configuration
(cct-configure-proof-general)
-(configure-delayed-coq)
+(configure-delayed-coq)
(defconst all-ancestors '("./b.v" "./c.v")
"All ancestors.")
@@ -151,3 +154,7 @@ situations. See Coq issue 15773."
(cct-unmodified-change-times vo-times))
(cct-older-change-times vo-times))
))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/009-failure-processing/runtest.el b/ci/compile-tests/009-failure-processing/runtest.el
index 1835eeb69..bc8c76945 100644
--- a/ci/compile-tests/009-failure-processing/runtest.el
+++ b/ci/compile-tests/009-failure-processing/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
;;
@@ -13,8 +15,8 @@
;; ert tests for parallel background compilation for Coq
;;
;; Test a partially successful and partially failing compilation with
-;; coq-compile-keep-going. Check that the right files are compiled,
-;; locked and unlocked. Check also the case, where unlocking of failed
+;; coq-compile-keep-going. Check that the right files are compiled,
+;; locked and unlocked. Check also the case, where unlocking of failed
;; files must be delayed, because some earlier successful require job
;; has not yet locked its ancestors.
;;
@@ -36,8 +38,8 @@
;;
;; Rb, Rc and Rd are three different require commands in file a. The
;; dependency e -> b is not present in test 5 and test 10 (but in all
-;; other tests). The error always happens in file g, for test 1-5 with
-;; coqdep, for tests 6-10 with coqc. There are 10 tests, each with
+;; other tests). The error always happens in file g, for test 1-5 with
+;; coqdep, for tests 6-10 with coqc. There are 10 tests, each with
;; slighly different delays, in 10 versions of the sources, e.g.,
;; a1-a10, b1-b10, and so on.
;;
@@ -58,14 +60,14 @@
;; 9: RB is ready and Rd is queue waiting
;; 10: without dependency b -> e: Rc, Rd are queue waiting, b finishes last
-
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
;;; set configuration
(cct-configure-proof-general)
-(configure-delayed-coq)
+(configure-delayed-coq)
(defconst pre-b-ancestors '("b" "f")
"Ancestors of b without suffixes.")
@@ -76,8 +78,8 @@
(defun pre-not-compiled (n)
"List of file name stems for which coqc must not be called.
Files for which coqc must not be called have an ``X'' in
-coqc-delay. For such files `compile-test-start-delayed' would
-create a ``.X'' file, whose absense is checked in the test."
+coqc-delay. For such files `compile-test-start-delayed' would
+create a ``.X'' file, whose absence is checked in the test."
(cond
((< n 6) '("g" "c"))
(t '("c"))))
@@ -140,3 +142,7 @@ create a ``.X'' file, whose absense is checked in the test."
(ert-deftest cct-failure-processing-08 () (test-failure-processing 8))
(ert-deftest cct-failure-processing-09 () (test-failure-processing 9))
(ert-deftest cct-failure-processing-10 () (test-failure-processing 10))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/010-coqdep-errors/runtest.el b/ci/compile-tests/010-coqdep-errors/runtest.el
index 3e6f423b9..03887b29d 100644
--- a/ci/compile-tests/010-coqdep-errors/runtest.el
+++ b/ci/compile-tests/010-coqdep-errors/runtest.el
@@ -1,4 +1,6 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
;;
;; © Copyright 2024 Hendrik Tews
;;
@@ -13,7 +15,7 @@
;; ert tests for parallel background compilation for Coq
;;
;; Test that parallel background compilation reliably detects coqdep
-;; errors. There are three tests that check the following coqdep errors:
+;; errors. There are three tests that check the following coqdep errors:
;; - coqdep on a require fails because of a missing library (using a.v)
;; - coqdep on a dependency fails because of a syntax error (using b.v)
;; - coqdep on a dependency fails because of a missing library (using d.v)
@@ -24,6 +26,7 @@
;; | |
;; c e
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
@@ -126,3 +129,7 @@
(should (and coqdep-errror-in-response
missing-module-in-response
(not dependency-in-coq)))))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/011-current-buffer/runtest.el b/ci/compile-tests/011-current-buffer/runtest.el
index 0e7225009..c30936f7a 100644
--- a/ci/compile-tests/011-current-buffer/runtest.el
+++ b/ci/compile-tests/011-current-buffer/runtest.el
@@ -1,5 +1,7 @@
-;; This file is part of Proof General. -*- lexical-binding: t; -*-
-;;
+;;; runtest.el --- Test -*- lexical-binding: t; -*-
+;;
+;; This file is part of Proof General.
+;;
;; © Copyright 2024 Hendrik Tews
;;
;; Authors: Hendrik Tews
@@ -22,7 +24,7 @@
;; b
;;
;; Files c and d are completely independent of file a and file b and
-;; not processed by Coq. The idea is that files c or d come from a
+;; not processed by Coq. The idea is that files c or d come from a
;; different project that uses a different `coq-compiler' or
;; `coq-dependency-analyzer', see also PG issue #797. These different
;; local settings should not confuse the ongoing background
@@ -30,19 +32,20 @@
;; File c sets `coq-compiler' as local variable and file d sets
;; `coq-dependency-analyzer' as local variable.
+;;; Code:
;; require cct-lib for the elisp compilation, otherwise this is present already
(require 'cct-lib "ci/compile-tests/cct-lib")
;;; set configuration
(cct-configure-proof-general)
-(configure-delayed-coq)
+(configure-delayed-coq)
(defvar switch-buffer-while-waiting nil
"Switch buffer in busy waiting hooks when t.
Whether the hook functions `switch-to-other-buffer-while-waiting'
and `switch-back-after-waiting' switch to some other buffer or
-not is controled by this variable. If t, switch to the buffer in
+not is controlled by this variable. If t, switch to the buffer in
`cdv-buffer' before starting busy waiting and switch back to the
buffer in `av-buffer' after busy waiting.")
@@ -56,7 +59,7 @@ See `switch-buffer-while-waiting'.")
(defun switch-to-other-buffer-while-waiting ()
"Hook to switch current buffer before busy waiting.
-Hook function for `cct-before-busy-waiting-hook'. Switches to
+Hook function for `cct-before-busy-waiting-hook'. Switches to
`cdv-buffer' if `switch-buffer-while-waiting' is t."
(when (and switch-buffer-while-waiting cdv-buffer)
(message "Switch to buffer c.v while busy waiting")
@@ -64,7 +67,7 @@ Hook function for `cct-before-busy-waiting-hook'. Switches to
(defun switch-back-after-waiting ()
"Hook to switch current buffer back after busy waiting.
-Hook function for `cct-after-busy-waiting-hook'. Switches back to
+Hook function for `cct-after-busy-waiting-hook'. Switches back to
`av-buffer' if `switch-buffer-while-waiting' is t."
(when (and switch-buffer-while-waiting av-buffer)
(message "Switch back to buffer a.v after busy waiting")
@@ -149,7 +152,7 @@ variables from the original scripting buffer, see also PG issue
(ert-deftest test-current-buffer-coqdep ()
"Check that dependency analysis uses the right local variables.
Dependency analysis during parallel background compilation (i.e.,
-runing `coqdep` on dependencies) should use the local variables
+running `coqdep` on dependencies) should use the local variables
from the original scripting buffer, see also PG issue #797."
(unwind-protect
(progn
@@ -203,7 +206,7 @@ from the original scripting buffer, see also PG issue #797."
(ert-deftest test-current-buffer-coqc ()
"Check that compilation of dependencies uses the right local variables.
Compilation of dependencies during parallel background
-compilation (i.e., runing `coqc` on dependencies) should use the
+compilation (i.e., running `coqc` on dependencies) should use the
local variables from the original scripting buffer, see also PG
issue #797.
@@ -264,3 +267,7 @@ switch to buffer c.v, which sets `coq-compiler' but leaves
(set-buffer-modified-p nil))
(kill-buffer buf)))
(setq switch-buffer-while-waiting nil)))
+
+(provide 'runtest)
+
+;;; runtest.el ends here
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index 76e9b2552..18d9777f0 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -1,3 +1,4 @@
+;;; cct-lib.el --- Background compilation test helpers
;; This file is part of Proof General.
;;
;; © Copyright 2020 - 2021 Hendrik Tews
@@ -16,17 +17,19 @@
;; This file contains common definitions for the automated tests of
;; parallel background compilation.
-;; Require some libraries for the elisp compilation. When compiling,
+;;; Code:
+
+;; Require some libraries for the elisp compilation. When compiling,
;; nothing is loaded, but all Proof General directories are in the
-;; load path. When this file is loaded as part of a test, proof-site
+;; load path. When this file is loaded as part of a test, proof-site
;; has been loaded but only the generic subdir is in the load path.
;; This file references variables from coq-compile-common and
;; functions from proof-shell, therefore coq-compile-common must be
-;; required for compilation. When running a test, these files would be
-;; loaded anyway when the test visits the first Coq file. For
-;; executing tests, the coq subdir will only be added to the load path
-;; when the first Coq file is visited. Therefore we have to add it
-;; here via proof-ready-for-assistant. For compilation, we have to
+;; required for compilation. When running a test, these files would be
+;; loaded anyway when the test visits the first Coq file. For
+;; executing tests, the Coq subdir will only be added to the load path
+;; when the first Coq file is visited. Therefore we have to add it
+;; here via proof-ready-for-assistant. For compilation, we have to
;; require proof-site, otherwise proof-ready-for-assistant won't be
;; defined.
(require 'proof-site)
@@ -51,7 +54,7 @@ Evaluate Q only if P is non-nil."
`(or (not ,p) ,q))
(defun cct-list-subset (l1 l2)
- "Return t if all elements of L1 are in L2 (compared by `equal')"
+ "Return t if all elements of L1 are in L2 (compared by `equal')."
(let ((res t))
(while (and l1 res)
(unless (member (pop l1) l2)
@@ -62,7 +65,7 @@ Evaluate Q only if P is non-nil."
;; seq-set-equal-p is not present before emacs 26.
;; XXX consider seq-set-equal-p when emacs 25 support is dropped.
(defun cct-list-set-equal (l1 l2)
- "Return t if L1 and L2 contain the elements (compared by `equal')"
+ "Return t if L1 and L2 contain the elements (compared by `equal')."
(and (cct-list-subset l1 l2)
(cct-list-subset l2 l1)))
@@ -82,21 +85,21 @@ Changes the suffix from .v to .vo. V-SRC-FILE must have a .v suffix."
(defun cct-record-change-time (file)
"Return cons of FILE and its modification time.
-The modification time is an emacs time value, it's nil if file
+The modification time is an Emacs time value, it's nil if file
cannot be accessed."
(cons file (nth 5 (file-attributes file))))
(defun cct-record-change-times (files)
"Return an assoc list of FILES with their modification times.
-The modification time is an emacs time value, it's nil if file
+The modification time is an Emacs time value, it's nil if file
cannot be accessed."
(mapcar 'cct-record-change-time files))
(defun cct-split-change-times (file-change-times files)
"Split assoc list FILE-CHANGE-TIMES.
FILE-CHANGE-TIMES must be an assoc list and FILES must be a list
-of some of the keys of FILE-CHANGE-TIMES. This function returns
-two associations lists (as cons cell). The car contains those
+of some of the keys of FILE-CHANGE-TIMES. This function returns
+two associations lists (as cons cell). The car contains those
associations in FILE-CHANGE-TIMES with keys not in FILES, the cdr
contains those with keys in FILES."
(let (out in)
@@ -108,7 +111,7 @@ contains those with keys in FILES."
(defun cct-replace-last-word (line word)
"Replace last word in line LINE with WORD.
In current buffer, go to the end of line LINE and one word
-backward. Replace the word there with WORD."
+backward. Replace the word there with WORD."
(cct-goto-line line)
(end-of-line)
(backward-word)
@@ -119,7 +122,7 @@ backward. Replace the word there with WORD."
"Assert/retract to start of line LINE and wait until processing completed.
Runs `cct-before-busy-waiting-hook' and
`cct-after-busy-waiting-hook' before and after busy waiting for
-the prover. In many tests these hooks are not used."
+the prover. In many tests these hooks are not used."
(when cct--debug-tests
(message "assert/retrect to line %d in buffer %s" line (buffer-name)))
(cct-goto-line line)
@@ -161,9 +164,9 @@ Runs `cct-before-busy-waiting-hook' and
"Get THE vanilla span for line LINE, report an error if there is none.
PG uses a number of overlapping and non-overlapping spans (read
overlays) in the asserted and queue region of the proof buffer,
-see the comments in generic/proof-script.el. Spans of type
+see the comments in generic/proof-script.el. Spans of type
vanilla (stored at 'type in the span property list) are created
-for real commands (not for comments). They hold various
+for real commands (not for comments). They hold various
information that is used, among others, for backtracking.
This function returns the vanilla span that covers line LINE and
@@ -184,8 +187,8 @@ and `current-message' does not return anything."
(buffer-substring (point) (- (point-max) 1))))
(defun cct-check-locked (line locked-state)
- "Check that line LINE has locked state LOCKED-STATE
-LOCKED-STATE must be 'locked or 'unlocked. This function checks
+ "Check that line LINE has locked state LOCKED-STATE.
+LOCKED-STATE must be 'locked or 'unlocked. This function checks
whether line LINE is inside or outside the asserted (locked)
region of the buffer and signals a test failure if not."
(let ((locked (eq locked-state 'locked)))
@@ -216,7 +219,7 @@ region of the buffer and signals a test failure if not."
(defun cct-check-files-locked (line lock-state files)
"Check that all FILES at line number LINE have lock state LOCK-STATE.
-LOCK-STATE must be either 'locked or 'unlocked. FILES must be
+LOCK-STATE must be either 'locked or 'unlocked. FILES must be
list of file names."
(when cct--debug-tests
(message "check files %s at line %d: %s"
@@ -233,7 +236,7 @@ list of file names."
The comparison treats ANCESTORS as set but the file names must
be `equal' as strings.
-Ancestors are recoreded in the 'coq-locked-ancestors property of
+Ancestors are recorded in the 'coq-locked-ancestors property of
the vanilla spans of require commands, see the in-file
documentation of coq/coq-par-compile.el."
(let ((locked-ancestors
@@ -256,9 +259,9 @@ recorded before."
(defun cct-unmodified-change-times (file-time-assoc)
"Check that files in FILE-TIME-ASSOC have not been changed.
-FILE-TIME-ASSOC must be an association list of files and emacs
+FILE-TIME-ASSOC must be an association list of files and Emacs
times as returned by `cct-record-change-times' or
-`cct-split-change-times'. This function checks that the
+`cct-split-change-times'. This function checks that the
modification time of files in FILE-TIME-ASSOC equals the time
recorded in FILE-TIME-ASSOC, i.e., that the file has not been
changed since FILE-TIME-ASSOC has been recorded."
@@ -288,9 +291,9 @@ changed since FILE-TIME-ASSOC has been recorded."
(defun cct-older-change-times (file-time-assoc)
"Check that files exist and have been changed.
-FILE-TIME-ASSOC must be an association list of files and emacs
+FILE-TIME-ASSOC must be an association list of files and Emacs
times as returned by `cct-record-change-times' or
-`cct-split-change-times'. This function checks that the files in
+`cct-split-change-times'. This function checks that the files in
FILE-TIME-ASSOC do exist and that their modification time is more
recent than in the association list, i.e., they have been updated
or changed since recording the time in the association."
@@ -323,14 +326,14 @@ or changed since recording the time in the association."
other-locked-files other-locked-line)
"Perform various checks for recompilation in MAIN-BUF.
MAIN-BUF is a buffer, MAIN-LOCKED and MAIN-SUM-line are line
-numbers in that buffer. NEW-SUM is a number as string. VO-TIMES
-is an association list of files and emacs times as returned by
+numbers in that buffer. NEW-SUM is a number as string. VO-TIMES
+is an association list of files and Emacs times as returned by
`cct-record-change-times' or `cct-split-change-times'.
RECOMPILED-FILES is a list of some of the files in VO-TIMES.
REQUIRE-ANCESTORS is a list of cons cells, each cons containing a
line number in MAIN-BUF (which should contain a require) and a
list of ancestor files that should get registered in the span of
-that require. OTHER-LOCKED-FILES is a list of buffers and
+that require. OTHER-LOCKED-FILES is a list of buffers and
OTHER-LOCKED-LINE is a common line number in those files.
This function combines all the following tests in this order:
@@ -385,8 +388,8 @@ This function combines all the following tests in this order:
(defun configure-delayed-coq ()
"Configure PG to honor artificial delays in background compilation.
Configure Proof General to use coqdep-delayed and coqc-delayed
-from directory ../bin. These scripts delay the start of the real
-coqdep and coqc as specified in the Coq soure file, see
+from directory ../bin. These scripts delay the start of the real
+coqdep and coqc as specified in the Coq source file, see
../bin/compile-test-start-delayed.
This function uses relative file names and must be called in a
@@ -399,3 +402,5 @@ test subdirectory parallel to the bin directory."
'(coq-compiler "coqc-delayed"))))
(provide 'cct-lib)
+
+;;; cct-lib.el ends here
diff --git a/ci/simple-tests/coq-test-changes-in-comments.el b/ci/simple-tests/coq-test-changes-in-comments.el
index aa093b324..c9ffce90d 100644
--- a/ci/simple-tests/coq-test-changes-in-comments.el
+++ b/ci/simple-tests/coq-test-changes-in-comments.el
@@ -1,3 +1,5 @@
+;;; coq-test-changes-in-comments.el --- Test changes inside comments
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2025 Hendrik Tews
@@ -13,7 +15,8 @@
;; to the next comment the buffer is correctly retracted.
-;;; Coq source code for tests
+
+;;; Code:
(defconst coq-src-comment
"(*
@@ -402,7 +405,7 @@ process and undo. Requires `comment-style' to be set."
(transient-mark-mode 1)
;; Insert `coq-src-comment' with many undo boundaries in
- ;; between.
+ ;; between.
(mapc
(lambda (s)
(insert s)
@@ -516,3 +519,7 @@ definition aXXa is gone. Then process and undo. Requires
(set-buffer-modified-p nil)
(setq comment-style saved-comment-style))
(kill-buffer buffer)))))
+
+(provide 'coq-test-changes-in-comments)
+
+;;; coq-test-changes-in-comments.el ends here
diff --git a/ci/simple-tests/coq-test-coqtop-unavailable.el b/ci/simple-tests/coq-test-coqtop-unavailable.el
index 662823891..c326a3b42 100644
--- a/ci/simple-tests/coq-test-coqtop-unavailable.el
+++ b/ci/simple-tests/coq-test-coqtop-unavailable.el
@@ -1,3 +1,5 @@
+;;; coq-test-coqtop-unavailable.el --- Test for when coqtop is unavailable
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
@@ -13,6 +15,8 @@
;; unavailable.
+;;; Code:
+
(ert-deftest coqtop-unavailable ()
"Proof General can open Coq files even when coqtop is unavailable.."
(setq coq-prog-name "unavailable-program")
@@ -22,3 +26,7 @@
(find-file "simple.v")
(coq-prog-args))
+
+(provide 'coq-test-coqtop-unavailable)
+
+;;; coq-test-coqtop-unavailable.el ends here
diff --git a/ci/simple-tests/coq-test-goals-present.el b/ci/simple-tests/coq-test-goals-present.el
index 7faa37b02..da2a975d1 100644
--- a/ci/simple-tests/coq-test-goals-present.el
+++ b/ci/simple-tests/coq-test-goals-present.el
@@ -1,3 +1,5 @@
+;;; coq-test-goals-present.el --- Test that Proof General shows goals correctly in various situations
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
@@ -10,11 +12,13 @@
;;; Commentary:
;;
;; Test that Proof General shows goals correctly in various
-;; situations. Test also that in other situations the response buffer
+;; situations. Test also that in other situations the response buffer
;; contains the right output and is visible in two-pane mode.
-;; gloabal configuration for this file
+;; global configuration for this file
;; all tests in this file shall run in two-pane mode
+;;; Code:
+
(setq proof-three-window-enable nil)
;; Some Emacs versions run with a frame width of 10 in batch mode
;; inside the container. The line breaks make some regular expressions
@@ -28,10 +32,10 @@
(require 'coq-system)
(defconst coq--between-v814-v815 (and (coq--post-v814) (coq--pre-v816))
- "t if Coq is either 8.14 or 8.15")
+ "Non-nil if Coq is either 8.14 or 8.15.")
(defconst coq--post-8-20 (not (coq--version< (coq-version t) "9.0alpha"))
- "t if Coq is 9.0 or higher")
+ "Non-nil if Coq is 9.0 or higher.")
(message (concat "goal/response present tests run with Coq version %s; \n\t"
@@ -39,7 +43,7 @@
(coq-version t) coq--between-v814-v815 coq--post-8-20)
-;;; Coq source code for tests
+;;; Coq source code for tests
(defconst coq-src-proof
"
@@ -123,7 +127,7 @@ Definition eq_one (i : nat) := i = 1.
Lemma foo: (eq_one 1 -> False) -> False.
(* point A: first process to this point *)
Proof.
- intros H.
+ intros H.
intro.
(* point B: Then process the two intros - the second one
triggers an error. The goals should be updated to show the
@@ -175,7 +179,7 @@ Used in `check-response-present' for all `response-buffer-visible-*' tests.")
(* marker A *)
Qed.
"
- "Coq source for ert-deftest's error-message-visible-at-qed-*")
+ "Coq source for ert-deftest's error-message-visible-at-qed-*.")
(defconst coq-src-queuemode-for-show-require
(if coq--post-8-20
@@ -184,8 +188,8 @@ Used in `check-response-present' for all `response-buffer-visible-*' tests.")
"Require command to use lists.
Starting in 9.0 the standard library containing Coq.Lists.List is in a
separate opam package, which might not be installed in the testing
-container. There use only stuff from the prelude, which is contained in
-packate rocq-core.")
+container. There use only stuff from the prelude, which is contained in
+package rocq-core.")
(defconst coq-src-queuemode-for-show-remainder
"Open Scope list_scope.
@@ -212,9 +216,9 @@ Proof using. (* marker A *)
trivial.
"
"Main Coq source code for extend/retract tests during long running Show.
-Main parte of Coq source code for extend/retract tests during long
+Main part of Coq source code for extend/retract tests during long
running Show without the first Require command, which is in
-`coq-src-queuemode-for-show-require'. When unfolded, the function
+`coq-src-queuemode-for-show-require'. When unfolded, the function
build_tree generates big terms that take quite long to print.")
@@ -245,7 +249,7 @@ BUF should be a buffer as string or buffer object."
(defun goals-after-test (coq-src msg check-response-nonempty)
"Test that Proof General shows goals after processing COQ-SRC.
Process COQ-SRC in a new buffer in one step and check that the
-goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY
+goals buffer is not empty afterwards. If CHECK-RESPONSE-NONEMPTY
is non-nil, additionally check that the response buffer is
non-empty, i.e., shows some message, and is visible in some
window also in two-pane mode."
@@ -301,10 +305,10 @@ the goals buffer is expected to be empty."
(defun goals-buffer-should-get-reset (coq-src coq-stm msg)
"Check that the goals buffer is reset.
Put the string COQ-SRC into a buffer and assert until the first
-occurrence of COQ-STM, which should be a regular expression. At
-this point the goals buffer needs to contain something. Then
+occurrence of COQ-STM, which should be a regular expression. At
+this point the goals buffer needs to contain something. Then
assert to the end of COQ-SRC and check that the goals buffer has
-been reset. MSG is used in messages only. It shouls say after
+been reset. MSG is used in messages only. It should say after
which action the goals buffer should have been reset."
(message "Check that goals are reset after %s." msg)
(let (buffer)
@@ -374,11 +378,11 @@ which action the goals buffer should have been reset."
(defun update-goals-when-response (coq-src first-pos goal-2nd msg)
"Test goals are up-to-date after an error or a command that produces response.
Process COQ-SRC up to the line after the first match of regular
-expression FIRST-POS. At this point the goals buffer should not
-be empty. Process now COQ-SRC up to the end. If GOAL-2ND is a
+expression FIRST-POS. At this point the goals buffer should not
+be empty. Process now COQ-SRC up to the end. If GOAL-2ND is a
regular expression as a string, then check that the goals have
-been updated to contain a match for GOAL-2ND. If GOAL-2ND is no
-string, only check that the goals buffer is non-empty. In any
+been updated to contain a match for GOAL-2ND. If GOAL-2ND is no
+string, only check that the goals buffer is non-empty. In any
case, check that the response buffer is not empty and visible in
two-pane mode."
@@ -439,7 +443,7 @@ two-pane mode."
(ert-deftest goals-up-to-date-after-search-one-step ()
"Check that goals are still present before showing result of one search cmd.
-This test checks a single Search command inside a proof. After
+This test checks a single Search command inside a proof. After
processing that Search command alone, the goals buffer should not
be empty and the response buffer should contain something and be
visible in two-pane mode."
@@ -451,7 +455,7 @@ visible in two-pane mode."
(ert-deftest goals-updated-after-search-many-steps ()
"Check that goals are updated before showing result of search cmd.
This test checks several commands inside a proof with a final
-Search command. After processing these commands, the goals buffer
+Search command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
(update-goals-when-response coq-src-update-goal-after-search
@@ -461,7 +465,7 @@ something and be visible in two-pane mode."
(ert-deftest goals-up-to-date-after-check-one-step ()
"Check that goals are still present before showing result of one check cmd.
-This test checks a single Check command inside a proof. After
+This test checks a single Check command inside a proof. After
processing that Check command alone, the goals buffer should not
be empty and the response buffer should contain something and be
visible in two-pane mode."
@@ -473,7 +477,7 @@ visible in two-pane mode."
(ert-deftest goals-updated-after-check-many-steps ()
"Check that goals are updated before showing result of check cmd.
This test checks several commands inside a proof with a final
-Check command. After processing these commands, the goals buffer
+Check command. After processing these commands, the goals buffer
should have been updated and the response buffer should contain
something and be visible in two-pane mode."
(update-goals-when-response coq-src-update-goal-after-check
@@ -539,7 +543,7 @@ section variable and check that the error message is displayed."
(ert-deftest error-message-visible-at-qed-one-step ()
"Check that the error message is present for Qed.
-Run a proof that uses an undeclared section variable. Check that the
+Run a proof that uses an undeclared section variable. Check that the
error message is displayed when running Qed alone as single step."
(message "Check that the error message is present at Qed for single step.")
(check-error-at-qed "marker A"))
@@ -621,22 +625,22 @@ advice for `coq-guess-or-ask-for-string', such that functions such as
(defun check-response-present (query-fun line input-string response)
"Check response and visibility of the response buffer.
This function checks that `coq-Search' and similar functions display
-their response correctly. QUERY-FUN is the command to be tested, for
+their response correctly. QUERY-FUN is the command to be tested, for
instance `coq-Search', or some closure, if the command needs arguments,
-such as `coq-Check'. LINE is the line number up to which
+such as `coq-Check'. LINE is the line number up to which
`coq-src-report-response-check' is processed before QUERY-FUN is called.
INPUT-STRING is the user input that QUERY-FUN shall receive from the
-adviced `coq-guess-or-ask-for-string'. RESPONSE is for the content check
-of the response buffer. If RESPONSE is a string, it must be a regular
-expression for which a match is searched in the response buffer. If
+advised `coq-guess-or-ask-for-string'. RESPONSE is for the content check
+of the response buffer. If RESPONSE is a string, it must be a regular
+expression for which a match is searched in the response buffer. If
RESPONSE is not a string the response buffer must be empty.
Global configuration of this file ensures two-pane mode by setting
-`proof-three-window-enable' to `nil'. It inserts
+`proof-three-window-enable' to nil. It inserts
`coq-src-report-response-check' into some buffer, processes this up to
-line LINE, advices `coq-guess-or-ask-for-string' to return INPUT-STRING,
-and calls QUERY-FUN. It then checks, according to RESPONSE, that the
-response buffer is either empty or contains the expected result. The
+line LINE, advises `coq-guess-or-ask-for-string' to return INPUT-STRING,
+and calls QUERY-FUN. It then checks, according to RESPONSE, that the
+response buffer is either empty or contains the expected result. The
function further checks that the response buffer is visible in some
window."
(let (buffer pos)
@@ -694,12 +698,12 @@ window."
(kill-buffer buffer)))))
(ert-deftest response-buffer-visible-coq-search-something-inside-proof ()
- "Check response for coq-Search on (S (_ + _)) inside proof."
+ "Check response for `coq-Search' on (S (_ + _)) inside proof."
(message "Check response for Search (S (_ + _)) is shown inside proof")
(check-response-present #'coq-Search 6 "(S (_ + _))" "^plus_Sn_m: forall"))
-
+
(ert-deftest response-buffer-visible-coq-search-something-proof-end ()
- "Check response for coq-Search on (S (_ + _)) at proof end.
+ "Check response for `coq-Search' on (S (_ + _)) at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
(message "Check response for Search (S (_ + _)) is shown at proof end")
@@ -708,17 +712,17 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 7 "(S (_ + _))" "^plus_Sn_m: forall"))
(ert-deftest response-buffer-visible-coq-search-something-outside-proof ()
- "Check response for coq-Search on (S (_ + _)) outside any proof."
+ "Check response for `coq-Search' on (S (_ + _)) outside any proof."
(message "Check response for Search (S (_ + _)) is shown outside proofs")
(check-response-present #'coq-Search 2 "(S (_ + _))" "^plus_Sn_m: forall"))
-
+
(ert-deftest response-buffer-visible-coq-search-empty-inside-proof ()
- "Check empty response for coq-Search on 42 inside proof"
+ "Check empty response for `coq-Search' on 42 inside proof."
(message "Check empty response for Search 42 is shown inside proof")
(check-response-present #'coq-Search 6 "42" t))
(ert-deftest response-buffer-visible-coq-search-empty-proof-end ()
- "Check empty response for coq-Search on 42 at proof end.
+ "Check empty response for `coq-Search' on 42 at proof end.
Skipped for 8.14 and 8.15, there Coq reacts with an error when searching
in proof mode with no more goals."
(message "Check empty response for Search 42 at proof end")
@@ -727,26 +731,26 @@ in proof mode with no more goals."
(check-response-present #'coq-Search 7 "42" t))
(ert-deftest response-buffer-visible-coq-search-empty-outside-proof ()
- "Check empty response for coq-Search on 42 outside proof"
+ "Check empty response for `coq-Search' on 42 outside proof."
(message "Check empty response for Search 42 is shown outside proof")
(check-response-present #'coq-Search 2 "42" t))
(ert-deftest response-buffer-visible-coq-check-print-all-inside-poof ()
- "Check response for coq-Check on plus_n_Sm inside proof with printing all."
+ "Check response for `coq-Check' on plus_n_Sm inside proof with printing all."
(message
"Check response for Check plus_n_Sm proof with printing all")
(check-response-present
#'(lambda() (coq-Check t)) 6 "plus_n_Sm" "@eq nat (S (Nat.add"))
(ert-deftest response-buffer-visible-coq-check-print-all-poof-end ()
- "Check response for coq-Check on plus_n_Sm at proof end with printing all."
+ "Check response for `coq-Check' on plus_n_Sm at proof end with printing all."
(message
"Check response for Check plus_n_Sm at proof end with printing all")
(check-response-present
#'(lambda() (coq-Check t)) 7 "plus_n_Sm" "@eq nat (S (Nat.add"))
(ert-deftest response-buffer-visible-coq-check-print-all-outside-poof ()
- "Check response for coq-Check on plus_n_Sm outside proof with printing all."
+ "Check response for `coq-Check' on plus_n_Sm outside proof with printing all."
(message
"Check response for Check plus_n_Sm outside proof with printing all")
(check-response-present
@@ -756,12 +760,12 @@ in proof mode with no more goals."
(defun user-action-during-long-running-show (extend)
"Test to extend or retract during long running Show.
The source code for this test generates a goal that takes about half a
-second to print. When running completely silent, this printing happens
-inside a Show command added as priority item. The user should be able to
+second to print. When running completely silent, this printing happens
+inside a Show command added as priority item. The user should be able to
extend the queue region during this long running Show.
-This function can test both, extension (if EXTEND is not `nil') and
-retraction (if EXTEND is `nil') during a long running Show. Retraction
+This function can test both, extension (if EXTEND is not nil) and
+retraction (if EXTEND is nil) during a long running Show. Retraction
should fail with the error message \"Proof process busy!\". Extending
the queue should not fail.
@@ -853,3 +857,7 @@ queuemode assertion again, because Coq was not killed in the handler."
"Test retracting during a long running Show."
(message "Retract during a long running Show of the previous command")
(user-action-during-long-running-show nil))
+
+(provide 'coq-test-goals-present)
+
+;;; coq-test-goals-present.el ends here
diff --git a/ci/simple-tests/coq-test-omit-proofs.el b/ci/simple-tests/coq-test-omit-proofs.el
index 24cd16996..a95bb8d7f 100644
--- a/ci/simple-tests/coq-test-omit-proofs.el
+++ b/ci/simple-tests/coq-test-omit-proofs.el
@@ -1,3 +1,5 @@
+;;; coq-test-omit-proofs.el --- Test the omit proofs feature
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
@@ -18,13 +20,15 @@
;; - the proof has omitted color then
;; - stuff before the proof still has normal color
+;;; Code:
+
;; Load stuff for `coq--version<'
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(require 'coq-system)
(defconst coq--post-v809 (coq--post-v809)
- "t if Coq is more recent than 8.8")
+ "Non-nil if Coq is more recent than 8.8.")
(message "omit tests run with Coq version %s; post-v809: %s"
(coq-version t) coq--post-v809)
@@ -56,7 +60,7 @@ If so, return the first non-nil value returned by PRED."
(defun reset-coq ()
"Reset Coq and Proof General.
Do `proof-shell-exit' to kill Coq and reset the locked region and
-a lot of other internal state of Proof General. Used at the
+a lot of other internal state of Proof General. Used at the
beginning of the test when several tests work on the same Coq
source file."
(when (and (boundp 'proof-shell-buffer)
@@ -74,13 +78,13 @@ therefore have a higher priority."
(defun overlays-at-point-sorted ()
"Return overlays at point in decreasing order of priority.
-Works only if no overlay has a priority property. Same
+Works only if no overlay has a priority property. Same
'(overlays-at (point) t)', except that it also works on Emacs <= 25."
(sort (overlays-at (point) t) 'overlay-less))
(defun first-overlay-face ()
"Return the face of the first overlay/span that has a face property.
-Properties configured in that face are in effect. Properties not
+Properties configured in that face are in effect. Properties not
configured there may be taken from faces with less priority."
(list-some
(lambda (ov) (overlay-get ov 'face))
@@ -90,7 +94,7 @@ configured there may be taken from faces with less priority."
(ert-deftest omit-proofs-omit-and-not-omit ()
"Test the omit proofs feature.
-In particular, test that with proof-omit-proofs-option configured:
+In particular, test that with `proof-omit-proofs-option' configured:
- the proof _is_ processed when using a prefix argument
- in this case the proof has normal locked color
- without prefix arg, the proof is omitted
@@ -285,3 +289,7 @@ This test only checks the faces in the middle of the proof."
;; Proof with bullets and braces should be omitted
(should (search-backward "automatic test marker 9 " nil t))
(should (eq (first-overlay-face) 'proof-omitted-proof-face))))
+
+(provide 'coq-test-omit-proofs)
+
+;;; coq-test-omit-proofs.el ends here
diff --git a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
index cea7f0943..9a4a7b9c2 100644
--- a/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
+++ b/ci/simple-tests/coq-test-par-job-needs-compilation-quick.el
@@ -19,11 +19,11 @@
;; This file file contains tests for `coq-par-job-needs-compilation-quick'.
;; It specifies for all combinations of `coq-compile-quick', existing
;; files and relative file ages the required result and side effects
-;; of `coq-par-job-needs-compilation-quick'. There are more than 500
-;; single tests, which are all independent. One could therefore define
-;; each of these single tests as an ERT test. However, one line in
+;; of `coq-par-job-needs-compilation-quick'. There are more than 500
+;; single tests, which are all independent. One could therefore define
+;; each of these single tests as an ERT test. However, one line in
;; `coq--par-job-needs-compilation-tests' generates between 1 and 4 of
-;; such single tests. Therefore, making each an ERT test is probably
+;; such single tests. Therefore, making each an ERT test is probably
;; not worth the effort.
;;
;; Debugging hints: Set test--coq-par-only-test to the failing test
@@ -934,7 +934,7 @@ test the result and side effects with `assert'."
(defconst test--coq-par-only-test nil
"If non-nil, run this test only.
-Must be nil under normal circumstances. Can be set to a number
+Must be nil under normal circumstances. Can be set to a number
for debugging, then only this test number is run.")
@@ -967,7 +967,7 @@ for debugging, then only this test number is run.")
(defun test-coq-par-job-needs-compilation-quick-fun (dir)
"Check test data wellformedness and run all the tests."
(when coq--debug-auto-compilation
- (message "check coq--par-job-needs-compilation-tests invariant"))
+ (message "check coq--par-job-needs-compilation-tests invariant"))
(test-coq-par-test-data-invarint)
(setq test--coq-par-counter 1)
(mapc
@@ -981,9 +981,11 @@ for debugging, then only this test number is run.")
coq--par-job-needs-compilation-tests))
(ert-deftest test-coq-par-job-needs-compilation-quick ()
- "Run all tests for coq-par-job-needs-compilation-quick."
+ "Run all tests for `coq-par-job-needs-compilation-quick'."
;;(setq coq--debug-auto-compilation t)
(test-coq-par-job-needs-compilation-quick-fun
(make-temp-name "/tmp/coq-par-test")))
-;;; test-coq-par-job-needs-compilation-quick.el ends here
+(provide 'coq-test-par-job-needs-compilation-quick)
+
+;;; coq-test-par-job-needs-compilation-quick.el ends here
diff --git a/ci/simple-tests/coq-test-prelude-correct.el b/ci/simple-tests/coq-test-prelude-correct.el
index 2dca77cef..f58b7ee56 100644
--- a/ci/simple-tests/coq-test-prelude-correct.el
+++ b/ci/simple-tests/coq-test-prelude-correct.el
@@ -1,3 +1,5 @@
+;;; coq-test-prelude-correct.el --- Test that the Proof General prelude is correct
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2021 Hendrik Tews
@@ -18,20 +20,22 @@
;; This test shows different behaviour before 8.10. When the problem
;; is fixed, I expect that the version distinction is no longer
;; necessary and can be deleted.
-;;
+
+;;; Code:
+
;; Load stuff for `coq--version<'
(require 'proof-site)
(proof-ready-for-assistant 'coq)
(require 'coq-system)
(defconst coq--post-v810 (coq--post-v810)
- "t if Coq is more recent than 8.9")
+ "Non-nil if Coq is more recent than 8.9.")
(message "prelude tests run with Coq version %s; post-v810: %s"
(coq-version t) coq--post-v810)
-;;; Coq source code for tests
+;;; Coq source code for tests
(defconst coq-src-proof
"Check 1."
@@ -90,3 +94,7 @@ yield an error."
(with-current-buffer buffer
(set-buffer-modified-p nil))
(kill-buffer buffer)))))
+
+(provide 'coq-test-prelude-correct)
+
+;;; coq-test-prelude-correct.el ends here
diff --git a/ci/simple-tests/coq-test-proof-stat.el b/ci/simple-tests/coq-test-proof-stat.el
index 8ec4e25fb..f7c737bf3 100644
--- a/ci/simple-tests/coq-test-proof-stat.el
+++ b/ci/simple-tests/coq-test-proof-stat.el
@@ -1,3 +1,5 @@
+;;; coq-test-proof-stat.el --- Tests for proof-check-report and proof-check-annotate
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2024 Hendrik Tews
@@ -11,10 +13,12 @@
;;
;; Tests for proof-check-report and proof-check-annotate.
+;;; Code:
+
(defun reset-coq ()
"Reset Coq and Proof General.
Do `proof-shell-exit' to kill Coq and reset the locked region and
-a lot of other internal state of Proof General. Used at the
+a lot of other internal state of Proof General. Used at the
beginning of the test when several tests work on the same Coq
source file."
(when (and (boundp 'proof-shell-buffer)
@@ -84,3 +88,7 @@ Check that `proof-check-report' signals an error with the expected message."
(with-current-buffer buffer
(set-buffer-modified-p nil))
(kill-buffer buffer)))))
+
+(provide 'coq-test-proof-stat)
+
+;;; coq-test-proof-stat.el ends here
diff --git a/ci/simple-tests/coq-test-three-window.el b/ci/simple-tests/coq-test-three-window.el
index 4b407e954..be0475f58 100644
--- a/ci/simple-tests/coq-test-three-window.el
+++ b/ci/simple-tests/coq-test-three-window.el
@@ -1,3 +1,4 @@
+;;; coq-test-three-window.el --- Test starting Proof General in three-pane mode
;; This file is part of Proof General.
;;
;; © Copyright 2024 Hendrik Tews
@@ -13,27 +14,29 @@
;; (`proof-three-window-enable' is t and
;; `proof-three-window-mode-policy' is 'smart) used to fail with
;; "window ... too small for splitting" for frame heights less then
-;; three times `window-min-height' (which defaults to 4). The problem
+;; three times `window-min-height' (which defaults to 4). The problem
;; was relevant for Emacs 26.3, 27.1, and 27.2 running in batch mode
;; in docker containers, because they set their frame height to 9 (and
-;; their width to 10) in such environments. For this reason most Proof
+;; their width to 10) in such environments. For this reason most Proof
;; General CI tests disable three pane mode in one or the other way.
;;
;; This file tests that the internal function `proof-select-three-b'
-;; creates 3 windows if the frame height is big enough. Additionally,
+;; creates 3 windows if the frame height is big enough. Additionally,
;; it is tested that one user command
;; (`proof-toggle-active-scripting') that used to be affected by the
-;; bug does not signal an error, regardless of the frame size. Both
+;; bug does not signal an error, regardless of the frame size. Both
;; functions are tested with three different frame sizes: too small
;; for 3 windows, just big enough for 3 windows, and the default frame
;; size.
+;;; Code:
+
(require 'pg-response)
(defun reset-coq ()
"Reset Coq and Proof General.
Do `proof-shell-exit' to kill Coq and reset the locked region and
-a lot of other internal state of Proof General. Used at the
+a lot of other internal state of Proof General. Used at the
beginning of the test when several tests work on the same Coq
source file."
(when (and (boundp 'proof-shell-buffer)
@@ -45,9 +48,9 @@ source file."
(defun test-proof-select-three-b-for-height (height expect-error)
"Test `proof-select-three-b' in 3-pane mode for HEIGHT.
EXPECT-ERROR must be non-nil precisely if the frame height is
-expected to be too small for 3 windows. In this case nothing is
+expected to be too small for 3 windows. In this case nothing is
done here, because `proof-select-three-b' must not be called in
-such situations. Otherwise the function should not signal an
+such situations. Otherwise the function should not signal an
error and set up 3 windows."
(if expect-error
(message "Skip test-proof-select-three-b for height %d" height)
@@ -98,7 +101,7 @@ height is 9 when running in a docker container."
"Test `proof-toggle-active-scripting' in 3-pane mode for HEIGHT.
The function should never signal an error and afterwards there
should be 3 windows if the frame has enough space and 2
-otherwise. Argument NUM-WIN specifies the expected number of
+otherwise. Argument NUM-WIN specifies the expected number of
windows for HEIGHT."
(let ((proof-three-window-enable t)
(proof-three-window-mode-policy 'smart))
@@ -134,3 +137,7 @@ height is 9 when running in a docker container."
(< emacs-major-version 28))
2
3)))
+
+(provide 'coq-test-three-window)
+
+;;; coq-test-three-window.el ends here
diff --git a/ci/simple-tests/qrhl-test-input.el b/ci/simple-tests/qrhl-test-input.el
index 0f00e2bd7..c654dcafd 100644
--- a/ci/simple-tests/qrhl-test-input.el
+++ b/ci/simple-tests/qrhl-test-input.el
@@ -1,3 +1,5 @@
+;;; qrhl-test-input.el --- Tests related to the qRHL prover
+;;
;; This file is part of Proof General.
;;
;; © Copyright 2022 Dominique Unruh
@@ -12,6 +14,8 @@
;; Tests related to the qRHL prover
;;
+;;; Code:
+
(ert-deftest load-qrhl-input ()
:expected-result :passed
"Test that the qRHL input method loads without errors in .qrhl files"
@@ -22,3 +26,7 @@
;; are translated correctly. But I don't know how. (Dominique)
(should (string= current-input-method "qrhl"))
)
+
+(provide 'qrhl-test-input)
+
+;;; qrhl-test-input.el ends here
diff --git a/coq/coq-compile-common.el b/coq/coq-compile-common.el
index 2d5c761e9..b07ac1b91 100644
--- a/coq/coq-compile-common.el
+++ b/coq/coq-compile-common.el
@@ -125,14 +125,14 @@ This is the internal value, use
(defun coq-max-second-stage-setter (symbol new-value)
":set function for `coq-max-background-second-stage-percentage'.
-SYMBOL should be 'coq-max-background-second-stage-percentage"
+SYMBOL should be \\='coq-max-background-second-stage-percentage"
(set-default symbol new-value)
(setq coq--max-background-second-stage-percentage-shadow new-value)
(coq-set-max-second-stage-jobs))
(defun coq-max-jobs-setter (symbol new-value)
":set function for `coq-max-background-compilation-jobs'.
-SYMBOL should be 'coq-max-background-compilation-jobs"
+SYMBOL should be \\='coq-max-background-compilation-jobs"
(set-default symbol new-value)
(cond
((eq new-value 'all-cpus)
@@ -160,7 +160,7 @@ Ignore any quick setting for Coq versions before 8.5."
;;; user options and variables
(defgroup coq-auto-compile ()
- "Customization for automatic compilation of required files"
+ "Customization for automatic compilation of required files."
:group 'coq
:package-version '(ProofGeneral . "4.1"))
@@ -203,16 +203,16 @@ This option can be set/reset via menu
(defcustom coq-compile-quick 'quick-and-vio2vo
"Control quick compilation, vio2vo and vio/vo files auto compilation.
-When using coq < 8.11,
+When using Coq < 8.11,
this option controls whether ``-quick'' is used for parallel
background compilation and whether up-date .vo or .vio files are
used or deleted. Please use the customization system to change
this option to ensure that any ``-quick'' setting is ignored for
Coq before 8.5.
-Please customize `coq-compile-vos' for coq >= 8.11.
+Please customize `coq-compile-vos' for Coq >= 8.11.
-Note that ``-quick'' can be noticebly slower when your sources do
+Note that ``-quick'' can be noticeably slower when your sources do
not declare section variables with ``Proof using''. Note that
even if you do declare section variables, ``-quick'' is typically
slower on small files.
@@ -221,7 +221,7 @@ Use `no-quick', if you have not yet switched to
``Proof using''. Use `quick-no-vio2vo', if you want quick
recompilation without producing .vo files. Value
`quick-and-vio2vo' updates missing prerequisites with ``-quick''
-and starts vio2vo conversion on a subset of the availables
+and starts vio2vo conversion on a subset of the available
cores (see `coq-compile-vio2vo-percentage') when the quick
recompilation finished (but see below for a .vio .vo
incompatibility caveat). Note that all the previously described
@@ -275,14 +275,14 @@ This option can be set via menu
:set #'coq-compile-quick-setter)
(defun coq-compile-prefer-quick ()
- "Return t if a .vio file would be prefered."
+ "Return t if a .vio file would be preferred."
(or
(eq coq-compile-quick 'quick-no-vio2vo)
(eq coq-compile-quick 'quick-and-vio2vo)))
(defcustom coq-compile-vos nil
"Control fast compilation, skipping opaque proofs with ``-vos'' and ``-vok''.
-When using coq >= 8.11, this option controls whether parallel
+When using Coq >= 8.11, this option controls whether parallel
background compilation is done with ``-vos'', skipping opaque
proofs, thus being considerably faster and inconsistent.
@@ -301,12 +301,12 @@ The second stage ``-vok'' run starts in the background after
cores used for the first run (configured in
`coq-max-background-compilation-jobs').
-For upgrading, if this option is `nil' (i.e., not configured),
+For upgrading, if this option is nil (i.e., not configured),
then the value of `coq-compile-quick' is considered and vos
compilation is used when `coq-compile-quick' equals
`'quick-no-vio2vo'.
-For coq < 8.11 this option is ignored."
+For Coq < 8.11 this option is ignored."
:type
'(radio
(const :tag "unset, derive behavior from `coq-compile-quick'" nil)
@@ -342,7 +342,7 @@ This option can be set/reset via menu
(defcustom coq-max-background-compilation-jobs 'all-cpus
"Maximal number of parallel jobs, if parallel compilation is enabled.
Use the number of available CPU cores if this is set to
-'all-cpus. This variable is the user setting. The value that is
+\\='all-cpus. This variable is the user setting. The value that is
really used is `coq--internal-max-jobs'. Use `coq-max-jobs-setter'
or the customization system to change this variable. Otherwise
your change will have no effect, because `coq--internal-max-jobs'
@@ -372,7 +372,7 @@ is initialized from the now deprecated option
:set #'coq-max-second-stage-setter)
(defcustom coq-max-background-vio2vo-percentage nil
- "Deprecated. Please configure `coq-max-background-second-stage-percentage'.
+ "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
@@ -387,7 +387,7 @@ the ``-vok'' second stage was implemented."
"Delay in seconds before starting the second stage compilation.
The delay is applied to both ``-vok'' and vio2vo second stages.
For Coq < 8.11 and vio2vo delay helps to avoid running into a
-library inconsistency with 'quick-and-vio2vo, see Coq issue
+library inconsistency with \\='quick-and-vio2vo, see Coq issue
#5223.
For backward compatibility, if this option is not customized, it
@@ -398,7 +398,7 @@ is initialized from the now deprecated option
(defcustom coq-compile-vio2vo-delay nil
;; XXX replace coq-compile-vio2vo-delay in ../doc/ProofGeneral.texi
- "Deprecated. Please configure `coq-compile-second-stage-delay'.
+ "Deprecated. Please configure `coq-compile-second-stage-delay'.
This is the old configuration option for Coq < 8.11, used before
the ``-vok'' second stage was implemented."
:type 'number
@@ -464,23 +464,23 @@ 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
+\\='physical-dir that will be loaded, the Coq source file in
+\\='physical-dir whose object will be loaded, the qualified module
identifier that occurs in the \"Require\" command, and the file
that contains the \"Require\".")
(defcustom coq-compile-auto-save 'ask-coq
"Buffers to save before checking dependencies for compilation.
-There are two orthogonal choices: Firstly one can save all or only the coq
-buffers, where coq buffers means all buffers in coq mode except the current
+There are two orthogonal choices: Firstly one can save all or only the Coq
+buffers, where Coq buffers means all buffers in Coq mode except the current
buffer. Secondly, Emacs can ask about each such buffer or save all of them
unconditionally.
-This makes four permitted values: 'ask-coq to confirm saving all
-modified Coq buffers, 'ask-all to confirm saving all modified
-buffers, 'save-coq to save all modified Coq buffers without
-confirmation and 'save-all to save all modified buffers without
+This makes four permitted values: \\='ask-coq to confirm saving all
+modified Coq buffers, \\='ask-all to confirm saving all modified
+buffers, \\='save-coq to save all modified Coq buffers without
+confirmation and \\='save-all to save all modified buffers without
confirmation.
This option can be set via menu
@@ -529,7 +529,7 @@ List of regular expressions for directories in which ProofGeneral
should not compile modules. If a library file name matches one
of the regular expressions in this list then ProofGeneral does
neither compile this file nor check its dependencies for
-compilation. It makes sense to include non-standard coq library
+compilation. It makes sense to include non-standard Coq library
directories here if they are not changed and if they are so big
that dependency checking takes noticeable time. The regular
expressions in here are always matched against the .vo file name,
@@ -541,10 +541,10 @@ or not."
(defcustom coq-compile-coqdep-warnings '("+module-not-found")
"List of warning options passed to coqdep via `-w` for Coq 8.19 or later.
List of warning options to be passed to coqdep via command line
-switch `-w`, which is supported from Coq 8.19 onwards. This
+switch `-w`, which is supported from Coq 8.19 onward. This
option is ignored for a detected Coq version earlier than 8.19. A
minus in front of a warning disables the warning, a plus turns
-the warning into an error. This option should contain
+the warning into an error. This option should contain
'+module-not-found' to let Proof General reliably detect missing
modules via an coqdep error."
:type '(repeat string)
@@ -600,16 +600,16 @@ modules are matched separately with `coq-require-id-regexp'")
"Return t if time value TIME-1 is earlier or equal to TIME-2.
A time value is a list of two, three or four integers of the
form (high low micro pico) as returned by `file-attributes' or
-'current-time'. First element high contains the upper 16 bits and
+`current-time'. First element high contains the upper 16 bits and
the second low the lower 16 bits of the time."
(not (time-less-p time-2 time-1)))
(defun coq-max-dep-mod-time (dep-mod-times)
"Return the maximum in DEP-MOD-TIMES.
Argument DEP-MOD-TIMES is a list where each element is either a
-time value (see `time-less-or-equal') or 'just-compiled. The
+time value (see `time-less-or-equal') or \\='just-compiled. The
function returns the maximum of the elements in DEP-MOD-TIMES,
-where 'just-compiled is considered the greatest time value. If
+where \\='just-compiled is considered the greatest time value. If
DEP-MOD-TIMES is empty it returns nil."
(let ((max nil))
(while dep-mod-times
@@ -631,7 +631,7 @@ DEP-MOD-TIMES is empty it returns nil."
"Check whether ProofGeneral should handle compilation of LIB-OBJ-FILE.
Return t if ProofGeneral should skip LIB-OBJ-FILE and nil if
ProofGeneral should handle the file. For normal users it does,
-for instance, not make sense to let ProofGeneral check if the coq
+for instance, not make sense to let ProofGeneral check if the Coq
standard library is up-to-date. This function is always invoked
on the .vo file name, regardless whether the file would be
compiled with ``-quick'' or not."
@@ -695,7 +695,7 @@ Changes the suffix from .vo to .vok. VO-OBJ-FILE must have a .vo suffix."
;;; manage coq--compile-response-buffer
(defconst coq--compile-response-initial-content "-*- mode: compilation; -*-\n\n"
- "Content of `coq--compile-response-buffer' after initialization")
+ "Content of `coq--compile-response-buffer' after initialization.")
;; XXX apparently nobody calls this with display equal to nil
(defun coq-compile-display-error (command error-message display)
@@ -795,10 +795,10 @@ from `coq-compile-save-some-buffers' to
(defun coq-compile-save-buffer-filter ()
"Filter predicate for `coq-compile-save-some-buffers'.
See also `save-some-buffers'. Return t for buffers with major
-mode 'coq-mode' different from
+mode `coq-mode' different from
`coq-compile-buffer-with-current-require' and nil for all other
-buffers. We will also return nil if the buffer is ephemeral, or
-not backed by a file. The buffer to test must be current."
+buffers. We will also return nil if the buffer is ephemeral, or
+not backed by a file. The buffer to test must be current."
(and
(eq major-mode 'coq-mode)
(not (string-prefix-p " " (buffer-name)))
diff --git a/coq/coq-db.el b/coq/coq-db.el
index 680292d16..6c1b6aac0 100644
--- a/coq/coq-db.el
+++ b/coq/coq-db.el
@@ -29,7 +29,7 @@
(require 'diff-mode)
(defconst coq-syntax-db nil
- "Documentation-only variable, for coq keyword databases.
+ "Documentation-only variable, for Coq keyword databases.
Each element of a keyword database contains the definition of a \"form\", of the
form:
@@ -44,25 +44,25 @@ INSERT is the complete text of the form, which may contain holes denoted by
\"#\" or \"@{xxx}\".
If non-nil the optional STATECH specifies that the command is not state
-preserving for coq.
+preserving for Coq.
-If non-nil the optional KWREG is the regexp to colorize correponding to the
+If non-nil the optional KWREG is the regexp to colorize corresponding to the
keyword. ex: \"simple\\\\s-+destruct\" (\\\\s-+ meaning \"one or more spaces\").
-*WARNING*: A regexp longer than another one should be put FIRST. For example:
+*WARNING*: A regexp longer than another one should be put FIRST. For example:
(\"Module Type\" ... ... t \"Module\\s-+Type\")
(\"Module\" ... ... t \"Module\")
-Is ok because the longer regexp is recognized first.
+Is OK because the longer regexp is recognized first.
If non-nil the optional INSERT-FUN is the function to be called when inserting
-the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This
+the form (instead of inserting INSERT, except when using \\[expand-abbrev]). This
allows to write functions asking for more information to assist the user.
If non-nil the optional HIDE specifies that this form should not appear in the
menu but only in interactive completions.
-Example of what could be in your emacs init file:
+Example of what could be in your Emacs init file:
\(defvar coq-user-tactics-db
\\='(
@@ -77,7 +77,7 @@ new keyword to colorize.")
(defun coq-insert-from-db (db prompt &optional alwaysjump)
"Ask for a keyword, with completion on keyword database DB and insert.
Insert corresponding string with holes at point. If an insertion
-function is present for the keyword, call it instead. See
+function is present for the keyword, call it instead. See
`coq-syntax-db' for DB structure. If ALWAYSJUMP is non nil, jump to
the first hole even if more than one."
(let* ((tac (completing-read (concat prompt " (TAB for completion): ")
@@ -251,7 +251,7 @@ structure."
res))
(defcustom coq-holes-minor-mode t
- "*Whether to apply holes minor mode (see `holes-show-doc') in coq mode."
+ "*Whether to apply holes minor mode (see `holes-show-doc') in `coq-mode'."
:type 'boolean
:group 'coq)
@@ -307,12 +307,12 @@ See `coq-syntax-db' for DB structure."
(defface coq-symbol-binder-face
'((t :inherit font-lock-type-face :bold coq-bold-unicode-binders))
- "Face for unicode binders, by default a bold version of `font-lock-type-face'."
+ "Face for Unicode binders, by default a bold version of `font-lock-type-face'."
:group 'proof-faces)
(defface coq-symbol-face
'((t :inherit font-lock-type-face :bold coq-bold-unicode-binders))
- "Face for unicode binders, by default a bold version of `font-lock-type-face'."
+ "Face for Unicode binders, by default a bold version of `font-lock-type-face'."
:group 'proof-faces)
(defface coq-question-mark-face
@@ -337,19 +337,19 @@ See `coq-syntax-db' for DB structure."
'(
(((class color) (background light)) . (:background "light gray"))
(((class color) (background dark)) . (:background "gray" :foreground "black")))
- "Coq face for the (un)folding hypothesis button"
+ "Coq face for the (un)folding hypothesis button."
:group 'proof-faces)
(defface coq-button-face-pressed
'((((class color) (background light)) . (:background "gray"))
(((class color) (background dark)) . (:background "dim gray" :foreground "black")))
- "Coq face for the (un)folding hypothesis button"
+ "Coq face for the (un)folding hypothesis button."
:group 'proof-faces)
(defface coq-button-face-active
'((((class color) (background light)) . (:background "black" :foreground "white"))
(((class color) (background dark)) . (:background "grey24" :foreground "black")))
- "Coq face for the (un)folding hypothesis button"
+ "Coq face for the (un)folding hypothesis button."
:group 'proof-faces)
(defconst coq-solve-tactics-face 'coq-solve-tactics-face
@@ -373,22 +373,22 @@ Required so that \\='coq-symbol-binder-face is a proper facename")
(defface coq-diffs-added-face
'((t . (:inherit diff-refine-added)))
- "Face used to highlight added text in diffs"
+ "Face used to highlight added text in diffs."
:group 'proof-faces)
(defface coq-diffs-removed-face
'((t . (:inherit diff-refine-removed)))
- "Face used to highlight removed text in diffs"
+ "Face used to highlight removed text in diffs."
:group 'proof-faces)
(defface coq-diffs-added-bg-face
'((t . (:inherit diff-added)))
- "Face used to highlight unchanged text in lines showing added text in diffs"
+ "Face used to highlight unchanged text in lines showing added text in diffs."
:group 'proof-faces)
(defface coq-diffs-removed-bg-face
'((t . (:inherit diff-removed)))
- "Face used to highlight unchanged text in lines showing removed text in diffs"
+ "Face used to highlight unchanged text in lines showing removed text in diffs."
:group 'proof-faces)
(defvar coq-tag-map
diff --git a/coq/coq-diffs.el b/coq/coq-diffs.el
index 198a09f54..ba4b24bd8 100644
--- a/coq/coq-diffs.el
+++ b/coq/coq-diffs.el
@@ -28,7 +28,7 @@
(defun coq-insert-tagged-text (str)
"Insert text into the current buffer applying faces specified by tags.
-For example 'foo' inserts 'foo' in the buffer
+For example \\='foo\\=' inserts \\='foo\\=' in the buffer
and applies the appropriate face.
`coq-tag-map' defines the mapping from tag name to face."
diff --git a/coq/coq-indent.el b/coq/coq-indent.el
index aab99837f..76565a301 100644
--- a/coq/coq-indent.el
+++ b/coq/coq-indent.el
@@ -46,7 +46,7 @@ No context checking.")
;; 2:
;; [goalname]:
(defconst coq-goal-selector-regexp "\\(?:[0-9]+\\|\\[\\w+\\]\\)\\s-*:\\s-*"
- "regexp of goal selector in coq.")
+ "Regexp of goal selector in Coq.")
;;;;;;;;;;;;;;; FORWARD / BACKWARD REGEXP ;;;;;;;;;;;;;;;;;
;; These regexp are used to split the buffer into commands. They make
@@ -62,10 +62,10 @@ No context checking.")
;; NOTE: \\= here allows to fail when the user types a "." just after
;; an already played command with no space.
(defconst coq-simple-cmd-ender-prefix-regexp-forward "[^.]\\|\\=\\|\\.\\."
- "Used internally. Matches the allowed prefixes of coq \".\" command ending.")
+ "Used internally. Matches the allowed prefixes of Coq \".\" command ending.")
(defconst coq-simple-cmd-ender-prefix-regexp-backward "[^.]\\|\\.\\."
- "Used internally. Matches the allowed prefixes of coq \".\" command ending.")
+ "Used internally. Matches the allowed prefixes of Coq \".\" command ending.")
;; bullets must appear after a command end. So when splitting a buffer
@@ -85,7 +85,7 @@ No context checking.")
;; proof-script-command-end-regexp in coq.el
(defconst coq-period-end-command
(concat "\\(?:\\(?2:" coq-simple-cmd-ender-prefix-regexp-forward "\\)\\(?1:\\.\\)\\(?3:\\s-\\|\\}\\|\\'\\)\\)")
- "Matches coq regular syntax for ending a command (except bullets and curlies).
+ "Matches Coq regular syntax for ending a command (except bullets and curlies).
This should match EXACTLY command ending syntax. No false
positive should be accepted. \"...\" is matched as \".\" with a
@@ -161,7 +161,7 @@ There are 3 substrings (2 and 3 may be nil):
WARNING: False positive.
There are 3 substrings:
-* number 1 is the real coq ending string,
+* number 1 is the real Coq ending string,
* 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
@@ -184,7 +184,7 @@ precise regexp (but only when searching backward).")
"Matches end of commands, including bullets and curlies.
There are 3 substrings (2 and 3 may be nil):
-* number 1 is the real coq ending string,
+* number 1 is the real Coq ending string,
* 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
@@ -235,13 +235,13 @@ Return nil if not found."
(defun coq-search-comment-delimiter-backward ()
"Search backward for a comment start (return 1) or end (return -1).
- Return nil if not found."
+Return nil if not found."
(when (re-search-backward coq-comment-start-or-end-regexp nil 'dummy)
(if (looking-at coq-comment-start-regexp) 1 -1)))
(defun coq-skip-until-one-comment-backward ()
"Skips comments and normal text until finding an unclosed comment start.
- Return nil if not found. Point is moved to the the unclosed comment start
+Return nil if not found. Point is moved to the the unclosed comment start
if found, to (point-max) otherwise. Return t if found, nil otherwise."
(if (= (point) (point-min)) nil
(ignore-errors (backward-char 1)) ; if point is between '(' and '*'
@@ -366,7 +366,7 @@ Comments are ignored, of course."
;; with implicits --> this function is recursive
(cond
;; "{" can be prefixed by a goal selector (coq-8.8).
- ;; TODO: looking-back is supposed to be slow. Find something else?
+ ;; TODO: looking-back is supposed to be slow. Find something else?
((or (and (looking-at "{")(looking-back "[0-9]+\\s-*:\\s-*" nil t))
(and (looking-at ":\\s-*{")(looking-back "[0-9]+\\s-*" nil t))
(and (looking-at "[0-9]+:\\s-*{") nil t))
@@ -396,8 +396,8 @@ Comments are ignored, of course."
"Move to the first end of command found looking forward from point.
Point is put exactly after the ending token (but before matching
substring if present). If no end command is found, go as far as
-possible and return nil. End of command appearing in comments are
-ignored. This function makes use of the substring 1 of the command end
+possible and return nil. End of command appearing in comments are
+ignored. This function makes use of the substring 1 of the command end
regexp."
(if (looking-at comment-start-skip)
;; Handle comments
@@ -534,12 +534,12 @@ The point is put exactly before first non comment letter of the command."
;; (let ((initpoint (point))
;; (forward-char (coq-is-on-ending-context))
;; (command-found (coq-command-at-point nojumplines))
-;; res
+;; res
;; )
;; (if command-found (coq-find-real-start))
-;; (while (and command-found
+;; (while (and command-found
;; ;; need this second test even with nojumplines:
-;; (same-line (point) initpoint))
+;; (same-line (point) initpoint))
;; (setq res (cons command-found res))
;; (if (and (coq-script-parse-cmdend-forward)
;; ;(ignore-errors (forward-char 1) t);to fit in the "and"
@@ -779,7 +779,7 @@ The point is put exactly before first non comment letter of the command."
;; (defun coq-goal-count (l) (coq-add-iter l 'coq-indent-goal-command-p))
;; (defun coq-save-count (l)
-;; (coq-add-iter l (lambda (x)
+;; (coq-add-iter l (lambda (x)
;; (or (coq-save-command-p nil x)
;; (eq (proof-string-match "\\<\\(?:EndSubproof\\)\\>\\|}" x) 0)))))
@@ -788,7 +788,7 @@ The point is put exactly before first non comment letter of the command."
;; (eq (proof-string-match "\\<\\(?:Proof\\|BeginSubproof\\)\\>\\|{" x) 0))))
;; returns the difference between goal (and assimilate Proof and BeginSubproof) and
-;; save commands in a commands list. This is to
+;; save commands in a commands list. This is to
;; (defun coq-goal-save-diff-maybe-proof (l)
;; (let ((proofs (coq-proof-count l))
;; (saves (coq-save-count l))
@@ -805,7 +805,7 @@ The point is put exactly before first non comment letter of the command."
;; Use `coq-indent-expr-offset' to indent a line belonging to an expression."
;; (let ((diff-goal-save-current
;; (coq-goal-save-diff-maybe-proof (coq-commands-at-line t)))
-;; (diff-goal-save-prev
+;; (diff-goal-save-prev
;; (save-excursion
;; (goto-char prevpoint)
;; (coq-goal-save-diff-maybe-proof (coq-commands-at-line t))))
@@ -816,21 +816,21 @@ The point is put exactly before first non comment letter of the command."
;; ;(forward-char -1)
;; (looking-at coq-indent-close-regexp)))
;; (current-closing-beginning ; t if the closing is at start of the (current) line
-;; (save-excursion
+;; (save-excursion
;; (back-to-indentation)
;; (looking-at coq-indent-close-regexp))))
;; ;(message "currentkind,prevcol,prevpoint = %d , %d ,%d " kind prevcol prevpoint)
;; (cond
;; ((proof-looking-at-safe "\\") 0);; no indentation at "Proof ..."
-;; (t (* proof-indent
+;; (t (* proof-indent
;; (let ((res
;; (let ((a diff-goal-save-prev) (b diff-goal-save-current)
;; (a2 prev-closing-beginning) (b2 current-closing-beginning))
;; ;(message "a,b,a2,b2 = %d,%d,%S,%S" a b a2 b2)
;; (cond
;; ((and (>= a 0) (>= b 0)) a)
-;; ((and (>= a 0) (< b 0) b2) (+ a -1)) ; a + b
+;; ((and (>= a 0) (< b 0) b2) (+ a -1)) ; a + b
;; ((and (>= a 0) (< b 0) (not b2)) a)
;; ((and (< a 0) (< b 0) a2 b2) a) ; a +1 -1
;; ((and (< a 0) (< b 0) a2 (not b2)) (+ a 1))
diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el
index 2211c22d5..892130f99 100644
--- a/coq/coq-local-vars.el
+++ b/coq/coq-local-vars.el
@@ -29,11 +29,11 @@
PROJECT FILE
The recommended way of setting coqtop options (-I, -R and others)
-is to use a project file. See the coq documentation (\"generating
+is to use a project file. See the Coq documentation (\"generating
makefile\") for details. The default name of the project file is
\"_CoqProject\" (can be configured via `coq-project-filename')
and its content should be a list of options to be given to
-coq_makefile (one option per line). Here is an example:
+Coq_makefile (one option per line). Here is an example:
-R foo bar
-I foo2
@@ -58,12 +58,12 @@ end of the file.
We provide the following feature to help you:
\\[coq-ask-insert-coq-prog-name] builds a standard file variable
-list for a coq file by asking you some questions. It is
+list for a Coq file by asking you some questions. It is
accessible in the menu
`Coq' -> `COQ PROG (ARGS)' -> `Set coq prog *persistently*'.
You should be able to use this feature without reading the rest
-of this documentation, which explains how it is used for coq. For
+of this documentation, which explains how it is used for Coq. For
more precision, refer to the Emacs info manual at ((Emacs)File
Variables).
@@ -89,7 +89,7 @@ Other buffers can have their own value of
`coq-load-path' (probably coming from their own local variable
lists).
-If you use `make' for the compilation of coq modules you can set
+If you use `make' for the compilation of Coq modules you can set
`coq-compile-command' as local variable. For instance, if the
makefile is located in \".../dir\", you could set
diff --git a/coq/coq-mode.el b/coq/coq-mode.el
index 2bc1ec39e..d4462a5ef 100644
--- a/coq/coq-mode.el
+++ b/coq/coq-mode.el
@@ -53,7 +53,7 @@ instead of just \"coqtop\".
This must be a single program name with no arguments. See option
`coq-prog-args' to manually adjust the arguments to the Coq process.
See also `coq-prog-env' to adjust the environment.
-With then 2025 new CLI 'rocq', this command only return 'rocq'."
+With then 2025 new CLI \\='rocq\\=', this command only return \\='rocq\\='."
:type 'string
:group 'coq
:group 'coq-mode)
@@ -67,7 +67,7 @@ With then 2025 new CLI 'rocq', this command only return 'rocq'."
"/usr/local/lib/coq")))
(defconst coq-library-directory (get-coq-library-directory) ;; FIXME Should be refreshed more often
- "The coq library directory, as reported by \"coqtop -where\".")
+ "The Coq library directory, as reported by \"coqtop -where\".")
(defcustom coq-tags (expand-file-name "/theories/TAGS" coq-library-directory)
"The default TAGS table for the Coq library."
@@ -146,7 +146,7 @@ With then 2025 new CLI 'rocq', this command only return 'rocq'."
(defvar coq-outline-heading-end-regexp "\\.[ \t\n]")
(defun coq-near-comment-region ()
- "Return a list of the forme (BEG END).
+ "Return a list of the form (BEG END).
BEG,END being is the comment region near position PT.
Return nil if PT is not near a comment.
Near here means PT is either inside or just aside of a comment."
@@ -165,7 +165,7 @@ Near here means PT is either inside or just aside of a comment."
(defun coq-fill-paragraph-function (_n)
- "Coq mode specific fill-paragraph function. Fills only comment at point."
+ "Coq mode specific `fill-paragraph' function. Fills only comment at point."
(let ((reg (coq-near-comment-region)))
(when reg
(fill-region (car reg) (cadr reg))))
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index e0f0bf488..0a08fcc10 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -26,8 +26,8 @@
;; - fix -I current-dir argument for coqc invocations
;; - on error, try to put location info into the error message
;; - use file-attribute-modification-time and similar functions when
-;; dropping support for emacs 25 (emacs 26.1 released on 05/2018)
-;; - use define-error when dropping support for emacs 24 (25.1
+;; dropping support for Emacs 25 (Emacs 26.1 released on 05/2018)
+;; - use define-error when dropping support for Emacs 24 (25.1
;; released on 09/2016)
;;
;; Note that all argument computations inherit `coq-autodetected-version': when
@@ -455,7 +455,7 @@ names to compilation jobs, regardless of ``-quick''.")
Used to link top-level jobs with queue dependencies.")
(defvar coq--par-second-stage-in-progress nil
- "t iff vio2vo or vok is running in background.")
+ "Non-nil iff vio2vo or vok is running in background.")
(defvar coq--par-second-stage-delay-timer nil
"Holds the timer for the second stage delay.")
@@ -465,12 +465,12 @@ Used to link top-level jobs with queue dependencies.")
Assume the last top-level ``Require'' command is retired, but
executing the ``Require'' takes so long that the user can assert
a next ``Require'' and that the second require is retired before
-the first ``Require'' has been processed. In this case there are
+the first ``Require'' has been processed. In this case there are
two `coq-par-require-processed' callbacks active, of which the
-first one must be ignored. For each new callback this counter is
+first one must be ignored. For each new callback this counter is
incremented and, when there is a difference,
`coq-par-require-processed' does not start the second stage
-timer. In case the first callback gets executed before the second
+timer. In case the first callback gets executed before the second
require is retired, the race is detected with
`coq--last-compilation-job' without this counter.")
@@ -482,7 +482,7 @@ The names are only used for debugging.")
"Inform the cycle detection that there is a delayed top-level job.
The retirement of failing require jobs must be delayed until
`proof-action-list' is empty, to avoid retracting commands before
-the first failing require. This is done by adding the call to
+the first failing require. This is done by adding the call to
`coq-par-kickoff-queue-maybe' to the end of `proof-action-list'.
This variable is t during this time to disable cycle detection,
which is otherwise started when `coq--last-compilation-job' has
@@ -518,7 +518,7 @@ the result."
(defun coq-par-time-less (time-1 time-2)
"Compare extended times.
-The arguments can be an emacs time (a list of 2 to 4 integers,
+The arguments can be an Emacs time (a list of 2 to 4 integers,
see `current-time') or the symbol 'just-compiled, where the
latter is greater then everything else."
(cond
@@ -681,8 +681,8 @@ Use `coq-par-second-stage-enqueue',
(defun coq-par-find-dependency-circle-for-job (job path)
"Find a dependency cycle in the dependency subtree of JOB.
-Do a depth-first-search to find the cycle. JOB is the current
-node and PATH the stack of visited nodes. Jobs in state
+Do a depth-first-search to find the cycle. JOB is the current
+node and PATH the stack of visited nodes. Jobs in state
'enqueue-coqc can be ignored, because they can never participate
in a cycle."
;; CORRECTNESS ARGUMENT FOR THIS FUNCTION
@@ -756,7 +756,7 @@ ignored, because they can never participate in a cycle."
(defun coq-par-coqdep-warning-arguments ()
"Return a fresh list with the warning command line arguments for coqdep.
-Warnings (`-w`) are supported in coqdep from 8.19 onwards.
+Warnings (`-w`) are supported in coqdep from 8.19 onward.
Therefore return the empty list for a detected Coq version
earlier than 8.19."
(if (and (coq--post-v818) (consp coq-compile-coqdep-warnings))
@@ -767,7 +767,7 @@ earlier than 8.19."
"Compute the command line arguments for invoking coqdep on LIB-SRC-FILE.
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
-load-path options to coqdep."
+`load-path' options to coqdep."
(nconc
(coq-coqdep-prog-args clpath (file-name-directory lib-src-file) (coq--pre-v85))
(copy-sequence coq-compile-extra-coqdep-arguments) ; copy for nconc
@@ -778,7 +778,7 @@ load-path options to coqdep."
"Compute the command line arguments for invoking coqc on LIB-SRC-FILE.
Argument CLPATH must be `coq-load-path' from the buffer
that triggered the compilation, in order to provide correct
-load-path options to coqdep."
+`load-path' options to coqdep."
(nconc (coq-coqc-prog-args clpath
(file-name-directory lib-src-file)
(coq--pre-v85))
@@ -787,12 +787,12 @@ load-path options to coqdep."
(defun coq-par-analyse-coq-dep-exit (status output command)
"Analyse output OUTPUT of coqdep command COMMAND with exit status STATUS.
-Returns the list of .vo dependencies if there is no error. Otherwise,
+Returns the list of .vo dependencies if there is no error. Otherwise,
writes an error message into `coq--compile-response-buffer', makes
this buffer visible and returns a string.
This function does always return .vo dependencies, regardless of the
-value of `coq-compile-quick'. If necessary, the conversion into .vio
+value of `coq-compile-quick'. If necessary, the conversion into .vio
or .vos files must be done elsewhere."
;; (when coq--debug-auto-compilation
;; (message "analyse coqdep output \"%s\"" output))
@@ -950,7 +950,7 @@ interrupt signal to the prover."
(setq prover-was-busy t))))
(defun coq-par-process-filter (process output)
- "Store OUTPUT from coq background compilation."
+ "Store OUTPUT from Coq background compilation."
(process-put process 'coq-process-output
(concat (process-get process 'coq-process-output) output)))
@@ -958,7 +958,7 @@ interrupt signal to the prover."
"Start asynchronous compilation job for COMMAND.
This function starts COMMAND with arguments ARGUMENTS for
compilation job JOB, making sure that CONTINUATION runs when the
-process finishes successfully. FILE-RM, if non-nil, denotes a
+process finishes successfully. FILE-RM, if non-nil, denotes a
file to be deleted when the process does not finish successfully."
;;(message "CPSP %s %s %s %s %s" command arguments continuation job file-rm)
(let ((process-connection-type nil) ; use pipes
@@ -985,7 +985,7 @@ file to be deleted when the process does not finish successfully."
(get job 'name) process-name
(if file-rm
(format "rm %s" file-rm)
- "no file removal")))
+ "no file removal")))
(when file-rm
(ignore-errors (delete-file file-rm)))
(signal 'coq-compile-error-command-start
@@ -1002,22 +1002,22 @@ file to be deleted when the process does not finish successfully."
(defun coq-par-process-sentinel (process event)
"Sentinel for all kinds of Coq background compilation processes.
-Runs when process PROCESS terminated because of EVENT. It
+Runs when process PROCESS terminated because of EVENT. It
determines the exit status and calls the continuation function
-that has been registered with that process. Normal compilation
+that has been registered with that process. Normal compilation
errors are reported with an error message inside the callback.
-Starts as many queued jobs as possible. The callback and queued
+Starts as many queued jobs as possible. The callback and queued
jobs are done with the 'script-buf as current buffer, such that
local variables and `default-directory' have correct values.
Second stage compilation jobs that have been killed, possibly
because the user triggered a next first stage compilation, are
-put back into `coq--par-second-stage-queue'. If, at the end, no
+put back into `coq--par-second-stage-queue'. If, at the end, no
job is running in the background but compilation has not been
finished, then, either second stage compilation finished (which
is reported), or there must be a cycle in the dependencies, which
-is found and reported here. The cycle detection is skipped, if
+is found and reported here. The cycle detection is skipped, if
the retirement of the last compilation job has been delayed per
-`coq--par-delayed-last-job'. All signals are caught inside this
+`coq--par-delayed-last-job'. All signals are caught inside this
function and reported appropriately."
(condition-case err
(if (process-get process 'coq-par-process-killed)
@@ -1126,9 +1126,9 @@ particular, `default-directory' have the correct values."
"Callback for `proof-action-list' to signal completion of the last Require.
This function ensures that second stage compilation starts after
`coq-compile-second-stage-delay' seconds after the last module has been
-loaded into Coq. When background compilation is successful, this
-callback is inserted with a dummy item into proof-action-list
-somewhere after the last require command. RACE-COUNTER is used to
+loaded into Coq. When background compilation is successful, this
+callback is inserted with a dummy item into `proof-action-list'
+somewhere after the last require command. RACE-COUNTER is used to
detect more than one active callback, see
`coq--par-second-stage-start-id'"
;; When the user asserts new stuff while the (previously) last
@@ -1144,7 +1144,7 @@ detect more than one active callback, see
(defun coq-par-callback-queue-item (callback)
"Create queue item containing just CALLBACK.
Create a queue item for `proof-action-list' containing just
-CALLBACK. CALLBACK must be a function taking a span as argument.
+CALLBACK. CALLBACK must be a function taking a span as argument.
The command list in the produced queue item is nil, therefore the
item will be processed as comment and only the callback will be called."
;; A proof-action-list item has the form of
@@ -1183,7 +1183,7 @@ is increased, such that DEPENDANT waits for the completion of DEPENDEE."
(defun coq-par-add-queue-dependency (dependee dependant)
"Add queue dependency from require job DEPENDEE to require job DEPENDANT.
The require item of DEPENDANT comes after those of DEPENDEE.
-Therefore DEPENDANT must wait for DEPENDEE to finish. "
+Therefore DEPENDANT must wait for DEPENDEE to finish."
(cl-assert (and (not (get dependant 'queue-dependant-waiting))
(not (get dependee 'queue-dependant)))
nil "queue dependency cannot be added")
@@ -1196,16 +1196,16 @@ Therefore DEPENDANT must wait for DEPENDEE to finish. "
(defun coq-par-job-needs-compilation-quick (job)
"Determine whether JOB needs to get compiled and do some side effects.
-This function contains most of the logic nesseary to support
-quick compilation according to `coq-compile-quick' for coq < 8.11. Taking
+This function contains most of the logic necessary to support
+quick compilation according to `coq-compile-quick' for Coq < 8.11. Taking
`coq-compile-quick' into account, it determines if a compilation
is necessary. The property 'required-obj-file is set either to
the file that we need to produce or to the up-to-date object
file. If compilation is needed, property 'use-quick is set to `vio' when
-quick/-vio will be used. If no compilation is needed, property
'obj-mod-time remembers the time stamp of 'required-obj-file.
-Indepent of whether compilation is required, .vo or .vio files
-that are in the way are deleted. Note that the coq documentation
+Independent of whether compilation is required, .vo or .vio files
+that are in the way are deleted. Note that the Coq documentation
does not contain a statement, about what file is loaded, if both
a .vo and a .vio file are present. To be on the safe side, I
therefore delete a file if it might be in the way. Sets the
@@ -1367,13 +1367,13 @@ therefore delete a file if it might be in the way. Sets the
(defun coq-par-job-needs-compilation-vos (job)
"Determine whether JOB needs to get compiled.
-This function decides whether JOB needs to get compiled for coq
->= 8.11 and whether a .vo or a .vos should be produced. For the
-latter, `coq-compile-vos' is consulted and, if that is `nil',
-coq-compile-quick, see `coq-compile-prefer-vos'. This function
-assumes that coq is used consistently and that a .vo file cannot
+This function decides whether JOB needs to get compiled for Coq
+>= 8.11 and whether a .vo or a .vos should be produced. For the
+latter, `coq-compile-vos' is consulted and, if that is nil,
+coq-compile-quick, see `coq-compile-prefer-vos'. This function
+assumes that Coq is used consistently and that a .vo file cannot
be present without a .vos file that has the same time stamp or
-has been created more recently. As result, this function sets the
+has been created more recently. As result, this function sets the
property 'use-quick to `vos' if JOB should be compiled with -vos.
If compilation is needed, 'required-obj-file is set.
If no compilation is needed, 'obj-mod-time is set to the time stamp of
@@ -1448,11 +1448,11 @@ the 'second-stage property on job to 'vok if necessary."
result))
(defun coq-par-job-needs-compilation (job)
- "Determine if JOB nees to get compiled and possibly do some side effects.
-This function calls `coq-par-job-needs-compilation-vos for coq >=
-8.11 and `coq-par-job-needs-compilation-quick' otherwise. Returns
+ "Determine if JOB needs to get compiled and possibly do some side effects.
+This function calls `coq-par-job-needs-compilation-vos for Coq >=
+8.11 and `coq-par-job-needs-compilation-quick' otherwise. Returns
t if a compilation is required and sets the 'use-quick property
-depending on wheter -quick/-vio or -vos should be used.
+depending on whether -quick/-vio or -vos should be used.
If compilation is needed, 'required-obj-file is set. Property
'obj-mod-time is set when no compilation is needed."
(if (coq--post-v811)
@@ -1464,7 +1464,7 @@ If compilation is needed, 'required-obj-file is set. Property
Apply `coq-par-collect-locked-file-ancestors' recursively to all
dependees to return those ancestors that are not yet asserted and
have not been returned yet by a previous invocation of this
-function on a different job. This function sets the
+function on a different job. This function sets the
'collect-visited property on all returned jobs, which should be
cleared before the next collection run."
;; (message "CLAD: job %s: dependees %s"
@@ -1478,8 +1478,8 @@ cleared before the next collection run."
(defun coq-par-collect-locked-file-ancestors (job)
"Collect locked, not-yet-found ancestors of JOB.
Return JOB if JOB is not asserted yet and has not been visited
-before by this function. Do the same recursively on all ancestors
-to return all not-yet-asserted ancestors of JOB. This function
+before by this function. Do the same recursively on all ancestors
+to return all not-yet-asserted ancestors of JOB. This function
sets the 'collect-visited property on all returned jobs, which
should be cleared before the next collection run."
;; (message "CLFA job %s cv %s ls %s"
@@ -1490,15 +1490,15 @@ should be cleared before the next collection run."
(cons job (coq-par-collect-locked-ancestors-dependees job))))
(defun coq-par-collect-locked-require-ancestors-rec (job)
- "Collect locked, not yet found ancestorors for require job JOB.
+ "Collect locked, not yet found ancestors for require job JOB.
Return all not yet asserted ancestors for successful jobs JOB as
-well as for failed jobs JOB. For successful jobs, the not yet
-asserted ancestors of preceeding require jobs have been collected
+well as for failed jobs JOB. For successful jobs, the not yet
+asserted ancestors of preceding require jobs have been collected
in a previous collection run and have been asserted back then.
For failed jobs, this is not the case and, moreover, ancestor
-unlocking can only be done when the last failing reqire job is
-retired. Therefore, for failed jobs, this function recureses into
-the preceeding require job, if it exists and is also marked as
+unlocking can only be done when the last failing require job is
+retired. Therefore, for failed jobs, this function recureses into
+the preceding require job, if it exists and is also marked as
failed."
(let ((this-anc (coq-par-collect-locked-ancestors-dependees job))
(q-dep (get job 'queue-dependee))
@@ -1510,13 +1510,13 @@ failed."
(defun coq-par-collect-locked-require-ancestors (job)
"Top-level ancestor collection function - collects not asserted ancestors.
Return all not yet asserted ancestors for successful jobs JOB as
-well as for failed jobs JOB. For failed require jobs JOB,
-additionally collect all asserted ancestors of all preceeding
-failed require jobs. This is necessary, because for failed jobs,
-unlocking only happens when the last require job is retired. The
+well as for failed jobs JOB. For failed require jobs JOB,
+additionally collect all asserted ancestors of all preceding
+failed require jobs. This is necessary, because for failed jobs,
+unlocking only happens when the last require job is retired. The
recursion internally uses property 'collect-visited to mark
already visited jobs in order to avoid an exponential blowup in
-graphs that are not trees. This property is reset here after
+graphs that are not trees. This property is reset here after
collection, such that its use stays internal."
(let ((ancs (coq-par-collect-locked-require-ancestors-rec job)))
(mapc (lambda (job) (put job 'collect-visited nil)) ancs)
@@ -1587,7 +1587,7 @@ jobs when they transition from 'waiting-queue to 'ready:
"Trigger `coq-par-kickoff-queue-maybe' from action list.
Simple wrapper around `coq-par-kickoff-queue-maybe' to ensure the
right scripting buffer is the current buffer and local variables
-and `default-directory' are taken from there. This function is
+and `default-directory' are taken from there. This function is
used to enter background compilation functions from
`proof-action-list'."
(with-current-buffer (get job 'script-buf)
@@ -1598,27 +1598,27 @@ used to enter background compilation functions from
(defun coq-par-kickoff-queue-maybe (job)
"Transition require job JOB to 'waiting-queue and maybe to 'ready.
-This function can only be called for require jobs. It further
+This function can only be called for require jobs. It further
must not be called if JOB is in state 'enqueued-coqdep or in
-state 'waiting-dep with some not yet finished dependencies. This
+state 'waiting-dep with some not yet finished dependencies. This
function is called when all dependencies of JOB are ready to put
-JOB into state 'waiting-dep. When in state 'waiting-dep, this
+JOB into state 'waiting-dep. When in state 'waiting-dep, this
function is also called, when the queue dependency of JOB has
transitioned to 'ready (inside this function).
-First JOB is put into state 'waiting-dep. If there is still a
+First JOB is put into state 'waiting-dep. If there is still a
queue dependency, nothing else happens and JOB waits until the
queue dependee calls this function again when it is ready.
If there is no queue dependency, then require job JOB must be
-retired and transition to 'ready. This means:
+retired and transition to 'ready. This means:
- for successful require jobs, ancestors are registered in the
'queue-span and marked as 'asserted in their 'lock-state
property
- processing of items in 'queueitems is started (if JOB is successful)
-- a possible queue dependant gets it's dependency cleared, and,
+- a possible queue dependent gets it's dependency cleared, and,
if possible the 'waiting-queue -> 'ready transition
- is (recursively) done for the dependant
+ is (recursively) done for the dependent
- if this job is the last top-level compilation
job (`coq--last-compilation-job') then the last compilation job
and `proof-second-action-list-active' are cleared and second stage
@@ -1626,7 +1626,7 @@ retired and transition to 'ready. This means:
- If compilation failed, the (failing) last top-level job is
delayed until `proof-action-list' is empty, possibly by
registering this call as a callback in an empty
- proof-action-list item. When proof-action-list is empty, the
+ proof-action-list item. When proof-action-list is empty, the
queue span is deleted, remaining spans are cleared and the
`proof-shell-busy' lock is freed."
(cl-assert (and (eq (get job 'type) 'require)
@@ -1730,7 +1730,7 @@ retired and transition to 'ready. This means:
(defun coq-par-compile-job-maybe (job)
"Compile JOB after dependencies are ready or start next transitions.
-This function can only be called for 'file jobs. It must also be
+This function can only be called for 'file jobs. It must also be
called for failed jobs to finish all necessary transitions.
First JOB is put into state 'enqueued-coqc. Then it is determined
if JOB needs compilation, what file must be produced (depending
@@ -1760,7 +1760,7 @@ transition 'enqueued-coqc -> 'ready is triggered."
(defun coq-par-decrease-coqc-dependency (dependant dependee-time)
"Clear Coq dependency and update dependee information in DEPENDANT.
This function handles a Coq dependency from child dependee to
-parent dependant when the dependee has finished compilation (ie.
+parent dependent when the dependee has finished compilation (ie.
is in state 'ready). DEPENDANT must be in state
'waiting-dep. The time of the most recent ancestor is updated, if
necessary using DEPENDEE-TIME. DEPENDEE-TIME must be an Emacs
@@ -1796,14 +1796,14 @@ This function can only be called for file jobs and it must also
be called for failed jobs to complete all necessary transitions.
This function is called after compilation has been finished (with
JUST-COMPILED being t) or after determining that compilation was
-not necessary or failed (with JUST-COMPILED being nil). This
+not necessary or failed (with JUST-COMPILED being nil). This
function sets 'youngest-coqc-dependency to the maximal (youngest)
time stamp of the vo file for this job and all its ancestors.
This function also decreases the dependency counter on all
-dependants, propagates 'youngest-coqc-dependency and
+dependents, propagates 'youngest-coqc-dependency and
starts any necessary state transitions on the
-dependants. Nothing special happens, if this job is successful
-but all its dependants are marked failed. Ancestor unlocking will
+dependents. Nothing special happens, if this job is successful
+but all its dependents are marked failed. Ancestor unlocking will
be done when the last require job is retired.
For the case that JUST-COMPILED is nil and that JOB has not
@@ -1848,7 +1848,7 @@ before."
(defun coq-par-start-coqdep-on-require (job)
"Start coqdep for require job JOB.
Write the require statement in JOB into a temporary file and
-start coqdep on it.
+start coqdep on it.
This function may be called asynchronously, if the require job
was queued."
@@ -1985,7 +1985,7 @@ used."
(defun coq-par-start-task (job)
"Start the background job for which JOB is waiting.
JOB was at the head of the compilation queue and now either
-coqdep, coqc, vio2vo or vok is started for it. This function may be called
+coqdep, coqc, vio2vo or vok is started for it. This function may be called
synchronously or asynchronously."
(let ((job-state (get job 'state)))
(cond
@@ -2018,7 +2018,7 @@ This function may be called synchronously or asynchronously."
"Start NEW-JOB or put it into the queue of waiting jobs.
NEW-JOB goes already into the waiting queue, if the number of
background jobs is one below the limit. This is in order to leave
-room for Proof General. This function might be called
+room for Proof General. This function might be called
synchronously or asynchronously."
(if (< (1+ coq--current-background-jobs) coq--internal-max-jobs)
(coq-par-start-task new-job)
@@ -2028,7 +2028,7 @@ synchronously or asynchronously."
"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
-nil. Argument SCRIPT-BUF must be the script buffer that caused
+nil. Argument SCRIPT-BUF must be the script buffer that caused
the background compilation."
(let ((new-job (make-symbol "coq-compile-job-symbol")))
(put new-job 'name (format "job-%d" coq--par-next-id))
@@ -2046,19 +2046,19 @@ the background compilation."
(defun coq-par-create-require-job (clpath require-items require-span script-buf)
"Create a new require job for REQUIRE-SPAN.
-Create a new require job and initialize its fields. CLPATH is the
+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 following the
REQUIRE-SPAN, they are temporarily stored in the new require job
-outside of `proof-action-list'. SCRIPT-BUF must be the script
-buffer that caused the background compilation. It is stored in
-property 'script-buf and propagated to all dependent jobs. This
+outside of `proof-action-list'. SCRIPT-BUF must be the script
+buffer that caused the background compilation. It is stored in
+property 'script-buf and propagated to all dependent jobs. This
buffer is made current in all sentinels and other asynchronously
called functions to ensure local variables and, in particular,
`default-directory' are correct.
-This function is called synchronously when asserting. The new
+This function is called synchronously when asserting. The new
require job is neither started nor enqueued here - the caller
must do this."
(let* ((coq-load-path clpath)
@@ -2079,15 +2079,15 @@ must do this."
(defun coq-par-create-file-job (module-vo-file clpath dep-src-file script-buf)
"Create a new file job for MODULE-VO-FILE.
DEP-SRC-FILE is the source file whose coqdep output we are just
-processing and which depends on MODULE-VO-FILE. This argument is
+processing and which depends on MODULE-VO-FILE. This argument is
only used in the error message, when MODULE-VO-FILE happens to
coincide with the current scripting buffer (which means we
-detected a dependency cycle). SCRIPT-BUF must be the current
+detected a dependency cycle). SCRIPT-BUF must be the current
scripting buffer and CLPATH must be the load path configured in
there, see also `coq-par-create-require-job'.
If there is a file job for MODULE-VO-FILE, just return this.
-Otherwise, create a new file job and initialize its fields. In
+Otherwise, create a new file job and initialize its fields. In
particular, initialize its 'lock-state property from the set of
as locked registered files in `proof-included-files-list'.
@@ -2123,9 +2123,9 @@ If a new job is created it is started or enqueued right away."
new-job))))
(defun coq-par-mark-queue-failing (job)
- "Mark require JOB and its queue dependants with 'failed.
+ "Mark require JOB and its queue dependents with 'failed.
Mark JOB with 'failed and unlock ancestors as appropriate.
-Recurse for queue dependants."
+Recurse for queue dependents."
(unless (get job 'failed)
(put job 'failed t)
(cl-assert (not (eq (get job 'state) 'ready))
@@ -2136,8 +2136,8 @@ Recurse for queue dependants."
(coq-par-mark-queue-failing (get job 'queue-dependant)))))
(defun coq-par-mark-job-failing (job)
- "Mark all dependants of JOB as failing and unlock ancestors as appropriate.
-Set the 'failed property on all direct and indirect dependants of
+ "Mark all dependents of JOB as failing and unlock ancestors as appropriate.
+Set the 'failed property on all direct and indirect dependents of
JOB. Along the way, unlock ancestors as determined by
`coq-par-ongoing-compilation'."
(unless (get job 'failed)
@@ -2158,13 +2158,13 @@ coqdep error, the following actions are taken.
- temp-require-file for require jobs is deleted
- the job that started PROCESS is put into state 'waiting-dep
- a new job is created for every dependency and registered in the
- dependency tree of all jobs. For dependencies that are 'ready
+ dependency tree of all jobs. For dependencies that are 'ready
already, the most recent ancestor modification time is
- propagated. If a dependency is marked as failed the current job
+ propagated. If a dependency is marked as failed the current job
is also marked as failed.
- if there are no dependencies (especially if coqdep failed) or
all dependencies are ready already, the next transition is
- triggered. For file jobs the next transition goes to
+ triggered. For file jobs the next transition goes to
'enqueued-coqc, for require jobs it goes to 'waiting-queue.
- otherwise the current job is left alone until somebody
decreases its dependency count to 0.
@@ -2195,7 +2195,7 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
(get job 'temp-require-file))
dependencies-or-error))
(when (get job 'temp-require-file)
- (ignore-errors (delete-file (get job 'temp-require-file))))
+ (ignore-errors (delete-file (get job 'temp-require-file))))
(setq job-max-time (get job 'youngest-coqc-dependency))
(dolist (dep-vo-file dependencies-or-error)
(unless (coq-compile-ignore-file dep-vo-file)
@@ -2261,7 +2261,7 @@ behind PROCESS."
(defun coq-par-vok-continuation (process exit-status)
"Vok continuation function.
-Nothing to do in case of success. Otherwise display the errors."
+Nothing to do in case of success. Otherwise display the errors."
(let ((job (process-get process 'coq-compilation-job)))
(if (eq exit-status 0)
;; success - nothing to do
@@ -2278,7 +2278,7 @@ Nothing to do in case of success. Otherwise display the errors."
(defun coq-par-vio2vo-continuation (process exit-status)
"Vio2vo continuation function.
-Nothing to do in case of success. Otherwise display the errors."
+Nothing to do in case of success. Otherwise display the errors."
(let ((job (process-get process 'coq-compilation-job)))
(if (eq exit-status 0)
;; success - nothing to do
@@ -2304,7 +2304,7 @@ Nothing to do in case of success. Otherwise display the errors."
"Start compilation for the required modules in the car of REQUIRE-ITEMS.
REQUIRE-ITEMS is a list of queue items, eventually to be added to
`proof-action-list', that contains just one require command in
-the first element. This function starts the compilation process
+the first element. This function starts the compilation process
for all modules and their dependencies in this require command.
This function creates one require job for the require command,
@@ -2362,7 +2362,7 @@ reporting.
If `coq-compile-before-require' is non-nil, this function starts
the compilation (if necessary) of the dependencies
-ansynchronously in parallel in the background.
+asynchronously in parallel in the background.
If there already is a last compilation job (`coq--last-compilation-job')
then the queue region is extended, while some background
@@ -2370,7 +2370,7 @@ compilation is still running. In this case I have to preserve the
internal state. Otherwise the hash of the compilation jobs and
the ancestor hash are reinitialized.
-As next action the new queue items are splitted at each Require
+As next action the new queue items are split at each Require
command. The items before the first Require are appended to the
old last compilation job or put back into ‘proof-action-list’. The
remaining batches of items that each start with a Require are
@@ -2435,10 +2435,10 @@ This function is called synchronously when asserting."
"Coq function for `proof-shell-extend-queue-hook' doing parallel compilation.
If `coq-compile-before-require' is non-nil, this function starts
the compilation (if necessary) of the dependencies
-ansynchronously in parallel in the background. This function only
+asynchronously in parallel in the background. This function only
does the error checking/reporting for
`coq-par-preprocess-require-commands-internal', which does all
-the work. This function is called synchronously when asserting."
+the work. This function is called synchronously when asserting."
(when coq-compile-before-require
(condition-case err
(coq-par-preprocess-require-commands-internal)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index af0c133f9..42f93c36b 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -59,14 +59,14 @@ properly unlock ANCESTOR-SRC on retract."
(defun coq-seq-get-library-dependencies (lib-src-file &optional command-intro)
"Compute dependencies of LIB-SRC-FILE.
Invoke \"coqdep\" on LIB-SRC-FILE and parse the output to
-compute the compiled coq library object files on which
+compute the compiled Coq library object files on which
LIB-SRC-FILE depends. The return value is either a string or a
list. If it is a string then an error occurred and the string is
the core of the error message. If the return value is a list no
error occurred and the returned list is the (possibly empty) list
of file names LIB-SRC-FILE depends on.
-If an error occurs this funtion displays
+If an error occurs this function displays
`coq--compile-response-buffer' with the complete command and its
output. The optional argument COMMAND-INTRO is only used in the
error case. It is prepended to the displayed command.
@@ -111,7 +111,7 @@ break."
()))))
(defun coq-seq-compile-library (src-file)
- "Recompile coq library SRC-FILE.
+ "Recompile Coq library SRC-FILE.
Display errors in buffer `coq--compile-response-buffer'."
(message "Recompile %s" src-file)
(let ((coqc-arguments
@@ -141,7 +141,7 @@ Display errors in buffer `coq--compile-response-buffer'."
(defun coq-seq-compile-library-if-necessary (max-dep-obj-time src obj)
"Recompile SRC to OBJ if necessary.
-This function compiles SRC to the coq library object file OBJ
+This function compiles SRC to the Coq library object file OBJ
if one of the following conditions is true:
- a dependency has just been compiled
- OBJ does not exist
@@ -161,7 +161,7 @@ If this function decides to compile SRC to OBJ it returns
OBJ.
Note that file modification times inside Emacs have only a
-precisision of 1 second. To avoid spurious recompilations we do
+precision of 1 second. To avoid spurious recompilations we do
not recompile if the youngest object file of the dependencies and
OBJ have identical modification times."
(let (src-time obj-time)
@@ -188,7 +188,7 @@ OBJ have identical modification times."
(defun coq-seq-make-lib-up-to-date (coq-obj-hash span lib-obj-file)
"Make library object file LIB-OBJ-FILE up-to-date.
Check if LIB-OBJ-FILE and all it dependencies are up-to-date
-compiled coq library objects. Recompile the necessary objects, if
+compiled Coq library objects. Recompile the necessary objects, if
not. This function returns 'just-compiled if it compiled
LIB-OBJ-FILE. Otherwise it returns the modification time of
LIB-OBJ-FILE as time value (see `time-less-or-equal').
@@ -294,10 +294,10 @@ therefore the customizations for `compile' do not apply."
(coq-library-src-of-vo-file absolute-module-obj-file)))))
(defun coq-seq-map-module-id-to-obj-file (module-id _span &optional from)
- "Map MODULE-ID to the appropriate coq object file.
+ "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.
-This is probably slower but much simpler than modelling coq file
+This is probably slower but much simpler than modeling Coq file
loading inside ProofGeneral. Argument SPAN is only used for error
handling. It provides the location information of MODULE-ID for a
decent error message.
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index 5528c6558..d969a8020 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -19,10 +19,10 @@
;; Lexer.
-;; Due to the verycomplex grammar of Coq, and to the architecture of
-;; smie, we deambiguate all kinds of tokens during lexing. This is a
+;; Due to the very complex grammar of Coq, and to the architecture of
+;; smie, we disambiguate all kinds of tokens during lexing. This is a
;; complex piece of code but it allows for all smie goodies.
-;; Some examples of deambigations:
+;; Some examples of disambiguation:
;; - We distinguish ":=" from ":= inductive" to avoid the circular precedence
;; constraint ":= < | < ; < :=" where ":= < |" is due to Inductive
;; definitions, "| < ;" is due to tactics precedence, "; < :=" is due to
@@ -53,7 +53,7 @@
(defcustom coq-smie-monadic-tokens '((";;" . ";; monadic")("do" . "let monadic")("<-" . "<- monadic")(";" . "in monadic"));
"This contains specific indentation token pairs, similar to
-`coq-smie-user-tokens' but dedicated to monadic operators. These
+`coq-smie-user-tokens' but dedicated to monadic operators. These
tokens have no builtin syntax except the one defined by this
variable so that users can change the syntax at will.
@@ -75,22 +75,22 @@ Th goal of this variable is to give concrete syntax to these
:group 'coq)
(defcustom coq-smie-user-tokens nil
- "Alist of (syntax . token) pairs to extend the coq smie parser.
+ "Alist of (syntax . token) pairs to extend the Coq smie parser.
These are user configurable additional syntax for smie tokens. It
allows to define alternative syntax for smie token. Typical
example: if you define a infix operator \"xor\" you may want to
define it as a new syntax for token \"or\" in order to have the
-indentation rules of or applied to xor. Other exemple: if you
+indentation rules of or applied to xor. Other example: if you
want to define a new notation \"ifb\" ... \"then\" \"else\" then
you need to declare \"ifb\" as a new syntax for \"if\" to make
indentation work well.
-An example of cofiguration is:
+An example of configuration is:
(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\".
+respectively same priority and associativity as \"or\" and \"if\".
For monadic notations, see `coq-smie-monadic-tokens' instead."
:type '(alist :key-type string :value-type string)
@@ -567,7 +567,7 @@ The point should be at the beginning of the command name."
;; Com start is a token for the first word of a command (provided it is a word)
((save-excursion
- (and (smie-default-backward-token)
+ (and (smie-default-backward-token)
(coq-is-at-command-real-start)
(> (length tok) 0)
(or (string= "Lu" (get-char-code-property (aref tok 0) 'general-category))
@@ -932,7 +932,7 @@ The point should be at the beginning of the command name."
;; qualifier.
(let ((nxtnxt (char-after (+ (point) (length tok)))))
(if (eq nxtnxt ?\() ". selector"
- (if (eq nxtnxt ?}) ;; dot immediately followed by closesubproof.
+ (if (eq nxtnxt ?}) ;; dot immediately followed by closesubproof.
"."
(if (or (null nxtnxt) (eq (char-syntax nxtnxt) ?\ ))
;; command terminator: ". proofstart" et al
@@ -1044,7 +1044,7 @@ If it is set to 2 (default) it is as follows:
(defcustom coq-match-indent 2
"Number of space used to indent cases of a match expression.
If the \"|\" separator is used, indentation will be reduced by 2.
-For example the default value 2 makes indetation like this:
+For example the default value 2 makes indentation like this:
match n with
O => ...
@@ -1419,7 +1419,7 @@ whereas with a nil value you get
;; z t (* align with function foo + 2. *)
;; u v. (* align with arg z on bol of previous line *)
-;; More complex:
+;; More complex:
;; Definition foo :=
;; foo x (y
;; a b)
@@ -1479,8 +1479,8 @@ whereas with a nil value you get
;; otherwise things like this:
;; { tac1. }
;; { tac2. }
- ;; would be detected as function applications.
- (>= (point) limit)
+ ;; would be detected as function applications.
+ (>= (point) limit)
(push (point) positions)
(not (smie-indent--bolp))))
(save-excursion
@@ -1543,7 +1543,7 @@ KIND is the situation and TOKEN is the thing w.r.t which the rule applies."
("} subproof" 0) ;;shouldn't be captured by (:elem . args)?
(". proofstart" coq-indent-proofstart)
(". modulestart" coq-indent-modulestart)
- ;; decrement indentation when hanging
+ ;; decrement indentation when hanging
((and (or "tactic infix" "after :=") (guard (or (hang-p) (smie-rule-bolp)))) 0)
((and "->" (guard (hang-p))) 0) ((or ":=" "with inductive") 2)
((or "." "; equations" "in let" "in monadic" ";; monadic") 0)
diff --git a/coq/coq-syntax.el b/coq/coq-syntax.el
index c66b8107a..90f6287d9 100644
--- a/coq/coq-syntax.el
+++ b/coq/coq-syntax.el
@@ -1013,7 +1013,7 @@ They deserve a separate menu for sending them to Coq without insertion.")
;; (la fonction vernac_declare_module dans toplevel/vernacentries)
(defun coq-count-match (regexp str)
- "Count the number of max. non-overlapping substring of STR matching REGEXP.
+ "Count the number of max. non-overlapping substring of STR matching REGEXP.
Empty matches are counted once."
(let ((nbmatch 0) (pos 0) (end (length str))
(case-fold-search nil))
@@ -1307,12 +1307,12 @@ Very similar to `coq-omit-proof-admit-command', but without the dot."
"Anomaly[:.]"
"Toplevel input"
"\\ and around all messages except errors.
@@ -1431,14 +1431,14 @@ Used in `coq-cmd-prevents-proof-omission' to identify tactics
that only have proof-local effects.")
(defconst coq-braces-regexp "^\\({\\|}\\)$"
- "Regular expression matching braces used for focussing and unfocussing.
+ "Regular expression matching braces used for focusing and unfocusing.
Used in `coq-cmd-prevents-proof-omission' to identify tactics
that only have proof-local effects.")
(defcustom coq-cmd-force-next-proof-kept "Let"
"Instantiating for `proof-script-cmd-force-next-proof-kept'.
Regular expression for commands that prevent omitting the next
-proof. A Let declaration with an admitted proof yields a warning,
+proof. A Let declaration with an admitted proof yields a warning,
see Proof General issue #687 and Coq issue #17199. Therefore,
proofs for a Let declaration should not be omitted."
:type 'regexp
diff --git a/coq/coq-system.el b/coq/coq-system.el
index a895ebc57..c1fbee506 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -17,8 +17,8 @@
;;; Commentary:
;;
;; This file holds constants, options and some general functions for
-;; setting coq command arguments. Some code is dedicated as a light
-;; support for older versions of coq.
+;; setting Coq command arguments. Some code is dedicated as a light
+;; support for older versions of Coq.
;;
;;; Code:
@@ -56,7 +56,7 @@ On Windows you might need something like:
;; We just call "rocq" and look the error message that should mention
;; subcommands
(defun coq-detect-rocq-cli ()
- "return non nil if the detected coq/rocq executable obeys the rocq CLI."
+ "Return non nil if the detected Coq/Rocq executable obeys the Rocq CLI."
(let* ((coq-command (or proof-prog-name (coq-autodetect-progname))))
(condition-case nil
(with-temp-buffer
@@ -81,15 +81,15 @@ On Windows you might need something like:
(defcustom coq-compiler (coq-detect-coqc)
;FIXME
- "Command to invoke the coq compiler."
+ "Command to invoke the Coq compiler."
:type 'string
:safe 'stringp
:group 'coq)
(defcustom coq-pinned-version nil
- "Manual coq version override (rarely needed).
+ "Manual Coq version override (rarely needed).
There should be no need to set this value unless you use old trunk versions from
-the Coq github repository. For Coq versions with decent version numbers
+the Coq GitHub repository. For Coq versions with decent version numbers
Proof General detects the version automatically and adjusts itself. This
variable should contain nil or a version string."
:type 'string
@@ -295,7 +295,7 @@ Return nil if the version cannot be detected."
(t (signal (car err) (cdr err))))))))
(defun coq--supports-topfile ()
- "Return t if \"-topfile\" appears in coqtop options"
+ "Return t if \"-topfile\" appears in coqtop options."
(string-match "-topfile" coq-autodetected-help)
)
@@ -341,7 +341,7 @@ Set to t if you want this feature, but note that it is deprecated."
path)))
(defcustom coq-load-path nil
- "Non-standard coq library load path.
+ "Non-standard Coq library load path.
This list specifies the LoadPath extension for coqdep, coqc and
coqtop. Usually, the elements of this list are strings (for
\"-I\") or lists of two strings (for \"-R\" dir path and
@@ -351,7 +351,7 @@ The possible forms of elements of this list correspond to the 4
forms of include options (`-I' `-Q' and `-R'). An element can be
- A list of the form `(\\='ocamlimport dir)', specifying (in 8.5) a
- directory to be added to ocaml path (`-I').
+ directory to be added to Ocaml path (`-I').
- A list of the form `(\\='rec dir path)' (where dir and path are
strings) specifying a directory to be recursively mapped to the
logical path `path' (`-R dir path').
@@ -369,11 +369,11 @@ the form `(dir path)' are interpreted as `(rec dir path)'.
A plain string maps to -Q ... \"\" in 8.5, and -I ... in 8.4.
Under normal circumstances this list does not need to
-contain the coq standard library or \".\" for the current
+contain the Coq standard library or \".\" for the current
directory (see `coq-load-path-include-current').
-WARNING: if you use coq <= 8.4, the meaning of these options is
-not the same (-I is for coq path)."
+WARNING: if you use Coq <= 8.4, the meaning of these options is
+not the same (-I is for Coq path)."
:type '(repeat (choice (string :tag "simple directory without path (-Q \"\") in 8.5, -I in 8.4")
(list :tag
"recursive directory with path (-R ... ...)"
@@ -444,7 +444,7 @@ request compatibility handling of flags."
"Build the base list of include options for coqc, coqdep and coqtop.
The options list includes all entries from argument LOADPATH
\(which should be `coq-load-path' of the buffer that invoked the
-compilation) prefixed with suitable options and (for coq<8.5), if
+compilation) prefixed with suitable options and (for Coq<8.5), if
`coq-load-path-include-current' is enabled, the directory base of
FILE. The resulting list is fresh for every call, callers can
append more arguments with `nconc'.
@@ -586,9 +586,9 @@ path (including the -R lib options) (see `coq-load-path')."
;; _xxProject is not present? And/Or if its content seems ok?
;; \\` and \\' avoid matching "_CoqProject~" and such
(defcustom coq-project-file-regexp "\\`\\(_coqproject\\|_rocqproject\\)\\'"
- "The regexp matching file names which PG detects as coq/rocq project files.
+ "The regexp matching file names which PG detects as Coq/Rocq project files.
-It is used by `coq--default-project-find-file' in a case insensistive way."
+It is used by `coq--default-project-find-file' in a case insensitive way."
:type 'string
:safe 'stringp
:group 'coq)
@@ -597,8 +597,8 @@ It is used by `coq--default-project-find-file' in a case insensistive way."
(defun coq--default-project-find-file (dir)
"Default function for `coq-project-filename'.
-If DIR contains an acceptable coq/rocq project file, return it. Return
-nil otherwise. See `coq-project-filename'."
+If DIR contains an acceptable Coq/Rocq project file, return it. Return
+nil otherwise. See `coq-project-filename'."
(when (file-directory-p dir)
(let* ((case-fold-search t) (files (directory-files dir)))
(cl-find-if (lambda (s) (string-match coq-project-file-regexp s nil)) files))))
@@ -609,35 +609,34 @@ nil otherwise. See `coq-project-filename'."
See its default value `coq--default-project-find-file' for an example.
The function takes one argument, the name of a directory, and returns
-the name of a coq/rocq project file it contains if there is one. Return
+the name of a Coq/Rocq project file it contains if there is one. Return
nil otherwise.
-This is used to detect the coq project file (using
-`locate-dominating-file'). By default we accept _CoqProject and
-_RocqProject (and any case-variant of these) without checking coq/rocq
-version. If you want something smarter please redefine
+This is used to detect the Coq project file (using
+`locate-dominating-file'). By default we accept _CoqProject and
+_RocqProject (and any case-variant of these) without checking Coq/Rocq
+version. If you want something smarter please redefine
`coq-project-filename' directly by using:
-(setq coq-project-filename #'my-own-predicate)
+\(setq coq-project-filename #'my-own-predicate)
-About the coq/rocq project file (cf. Coq documentation on project files
+About the Coq/Rocq project file (cf. Coq documentation on project files
and \"makefile generation\"):
-The coq project file of a coq development should contain the arguments
-given to coq_makefile. In particular it contains the -I and -R
+The Coq project file of a Coq development should contain the arguments
+given to Coq_makefile. In particular it contains the -I and -R
options (preferably one per line). If `coq-use-coqproject' is
t (default) the content of this file will be used by Proof General to
infer the `coq-load-path' and the `coq-prog-args' variables that set the
coqtop invocation by Proof General. This is now the recommended way of
configuring the coqtop invocation. Local file variables may still be
-used to override the coq project file's configuration. .dir-locals.el
-files also work and override project file settings.
-"
+used to override the Coq project file's configuration. .dir-locals.el
+files also work and override project file settings."
:type 'function
:group 'coq)
(defun coq-find-project-file ()
- "Return '(buf alreadyopen) where buf is the buffer visiting coq project file.
+ "Return '(buf alreadyopen) where buf is the buffer visiting Coq project file.
alreadyopen is t if buffer already existed."
(when buffer-file-name
(let* ((projectfiledir
@@ -691,9 +690,9 @@ Returns a mixed list of option-value pairs and strings."
(defun coq--extract-prog-args (options)
"Extract coqtop arguments from _CoqProject options OPTIONS.
OPTIONS is a list or conses (switch . argument) and strings.
-Note that the semantics of the -arg flags in coq project files
+Note that the semantics of the -arg flags in Coq project files
are weird: -arg \"a b\" means pass a and b, separately, to
-coqtop. But -arg \"'a b'\" means to pass a and b together."
+coqtop. But -arg \"'a b'\" means to pass a and b together."
(let ((args nil))
(dolist (opt options)
(pcase opt
@@ -718,7 +717,7 @@ coqtop. But -arg \"'a b'\" means to pass a and b together."
(list 'recnoimport (expand-file-name path base-directory) alias))))
(defun coq--extract-load-path (options base-directory)
- "Extract loadpath from _CoqProject options OPTIONS.
+ "Extract LoadPath from _CoqProject options OPTIONS.
OPTIONS is a list or conses (switch . arguments) and strings.
Paths are taken relative to BASE-DIRECTORY."
(cl-loop for opt in options
diff --git a/coq/coq.el b/coq/coq.el
index 7d0f528b7..93e40eece 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -81,15 +81,15 @@
Please restart Proof General after changing this setting!
If enabled, run Coq completely silent (Set Silent) and only issue
-a show command when necessary to update the goals buffer. This
-behavior is new. If you experience strange effects, please report
-a bug and switch this flag off to return to old behavior. When
+a show command when necessary to update the goals buffer. This
+behavior is new. If you experience strange effects, please report
+a bug and switch this flag off to return to old behavior. When
disabled, Coq is dynamically switched to silent for longer lists
-of commands and switched to verbose before the last command. A
+of commands and switched to verbose before the last command. A
manual Show command (C-c C-p) is necessary if the last command
fails to update the goals buffer (e.g., if it is a comment or it
is not executed because some other command before failed, see
-also bug report #568). External proof tree display is only
+also bug report #568). External proof tree display is only
supported if this option is t."
:type 'boolean
:safe 'booleanp
@@ -102,7 +102,7 @@ These are appended at the end of `coq-shell-init-cmd'."
:group 'coq)
(defcustom coq-optimise-resp-windows-enable t
- "If non-nil (default) resize vertically response windw after each command."
+ "If non-nil (default) resize vertically response window after each command."
:type 'boolean
:group 'coq)
@@ -110,8 +110,8 @@ These are appended at the end of `coq-shell-init-cmd'."
(defcustom coq-search-blacklist-string ; add this? \"_ind\" \"_rect\" \"_rec\"
"\"Private_\" \"_subproof\""
"Initial strings to blacklist in requests to Coq environment.
-If you are setting this via emacs cutomization menus, you should
-restart Coq to see the effect. To change blacklist during a coq
+If you are setting this via Emacs customization menus, you should
+restart Coq to see the effect. To change blacklist during a Coq
development, please use \\[coq-change-search-blacklist-interactive]
instead (or menu: Coq/Settings/Search Blacklist)."
:type 'string
@@ -146,15 +146,15 @@ Namely, goals that do not fit in the goals window."
coq-user-init-cmd)
"Commands for initial Coq configuration, Coq variant of `proof-shell-init-cmd'.
List of commands sent to the Coq background process just after it
-has been started. This happens inside `proof-shell-config-done',
+has been started. This happens inside `proof-shell-config-done',
when the major mode `coq-shell-mode' is configured in the `*coq*'
buffer.
-Sets silent mode if `coq-run-completely-silent' is set. Note that
+Sets silent mode if `coq-run-completely-silent' is set. Note that
this constant is not updated when `coq-run-completely-silent' is changed.
In normal interaction, Coq is started because the user asserts
-some commands. Therefore the commands here are followed by those
+some commands. Therefore the commands here are followed by those
inserted inside `proof-assert-command-hook', respectively,
`coq-adapt-printing-width'.")
@@ -168,7 +168,7 @@ inserted inside `proof-assert-command-hook', respectively,
(defvar coq-shell-prompt-pattern
"\\(?:\n\\(?:[^\n\371]+\371\\|[^\n]+\\)\\)"
- "*The prompt pattern for the inferior shell running coq.")
+ "The prompt pattern for the inferior shell running Coq.")
;; FIXME da: this was disabled (set to nil) -- why?
;; da: 3.5: add experimental
@@ -187,9 +187,9 @@ inserted inside `proof-assert-command-hook', respectively,
;; \\|This subproof is complete
)
"*Regular expression indicating that the proof has been completed.
-Coq instance of `proof-shell-clear-goals-regexp'. Used in
+Coq instance of `proof-shell-clear-goals-regexp'. Used in
`proof-shell-process-urgent-message' to determine if the goals
-buffer shall be cleaned. Some of the messages recognized here are
+buffer shall be cleaned. Some of the messages recognized here are
not printed by Coq in silent mode, such that Proof General might
fail to delete the goals buffer.")
@@ -553,7 +553,7 @@ This is a subroutine of `proof-shell-filter'."
;; Use the statenumber inside the coq prompt to backtrack more easily
(defun coq-last-prompt-info (s)
- "Extract info from the coq prompt S. See `coq-last-prompt-info-safe'."
+ "Extract info from the Coq prompt S. See `coq-last-prompt-info-safe'."
(let ((lastprompt (or s (error "No prompt !!?")))
(regex
(concat ">\\(" coq-id-shy "\\) < \\([0-9]+\\) |\\(\\(?:" coq-id-shy
@@ -571,7 +571,7 @@ This is a subroutine of `proof-shell-filter'."
(defun coq-last-prompt-info-safe ()
- "Return a list with all informations from the last prompt.
+ "Return a list with all information from the last prompt.
The list contains in the following order the state number, the
proof stack depth, a list with the names of all pending proofs,
and as last element the name of the current proof (or nil if
@@ -648,7 +648,7 @@ and read by function `coq-empty-action-list-command'.")
(defun coq-set-state-infos ()
"Set the last locked span's state number to the number found last time.
This number is in the *last but one* prompt (variable `coq-last-but-one-statenum').
-If locked span already has a state number, then do nothing. Also updates
+If locked span already has a state number, then do nothing. Also updates
`coq-last-but-one-statenum' to the last state number for next time."
(if proof-shell-last-prompt
;; da: did test proof-script-buffer here, but that seems wrong
@@ -721,7 +721,7 @@ If locked span already has a state number, then do nothing. Also updates
;; proof-change-hook used above is not exactly called at right times).
(defun coq-find-and-forget (span)
- "Backtrack to SPAN. Using the \"BackTo n\" coq command."
+ "Backtrack to SPAN. Using the \"BackTo n\" Coq command."
(if (eq (span-property span 'type) 'proverproc)
;; processed externally (i.e. Require, etc), nothing to do
;; (should really be unlocked when we undo the Require).
@@ -744,7 +744,7 @@ If locked span already has a state number, then do nothing. Also updates
"Last goal that Emacs looked at.")
(defun coq-goal-hyp ()
- "Instanciation for `pg-topterm-goalhyplit-fn', see there."
+ "Instantiation for `pg-topterm-goalhyplit-fn', see there."
(cond
((looking-at "============================\n")
(goto-char (match-end 0))
@@ -758,7 +758,7 @@ If locked span already has a state number, then do nothing. Also updates
(t nil)))
(defun coq-state-preserving-p (cmd)
- "Instanciation for `proof-state-preserving-p', see there."
+ "Instantiation for `proof-state-preserving-p', see there."
;; (or
(proof-string-match coq-non-retractable-instruct-regexp cmd))
;; (and
@@ -768,14 +768,14 @@ If locked span already has a state number, then do nothing. Also updates
;; t))))
(defun coq-cmd-prevents-proof-omission (cmd)
- "Instanciation for `proof-script-cmd-prevents-proof-omission'.
+ "Instantiation for `proof-script-cmd-prevents-proof-omission'.
This predicate decides whether a command inside a proof might
have effects outside the proof, which would prohibit omitting the
proof, see `proof-script-omit-proofs'.
Commands starting lower case are deemed as tactics that have
-proof local effect only and so are bullets and braces. Everything
-else is checked against the STATECH field in the coq syntax data
+proof local effect only and so are bullets and braces. Everything
+else is checked against the STATECH field in the Coq syntax data
base, see coq-db.el."
(if (or (proof-string-match coq-lowercase-command-regexp cmd)
(proof-string-match coq-bullet-regexp cmd)
@@ -812,7 +812,7 @@ the *goals* buffer."
(defconst notation-print-kinds-table
'(("Print Scope(s)" 0) ("Print Visibility" 1))
- "Enumerates the different kinds of notation information one can ask to coq.")
+ "Enumerates the different kinds of notation information one can ask to Coq.")
(defun coq-PrintScope ()
"Show information on notations. Coq specific."
@@ -854,7 +854,7 @@ If C is nil, return nil."
(or (equal (char-syntax c) ?\.) (equal (char-syntax c) ?\_))))
(defun coq-grab-punctuation-left (pos)
- "Return a string made of punctuations chars found immediately before position POS."
+ "Return a string made of punctuation chars found immediately before position POS."
(let ((res nil)
(currpos pos))
(while (coq-is-symbol-or-punct (char-before currpos))
@@ -864,7 +864,7 @@ If C is nil, return nil."
(defun coq-grab-punctuation-right (pos)
- "Return a string made of punctuations chars found immediately after position POS."
+ "Return a string made of punctuation chars found immediately after position POS."
(let ((res nil)
(currpos pos))
(while (coq-is-symbol-or-punct (char-after currpos))
@@ -935,10 +935,10 @@ is nil (t by default)."
(if id id (concat "\"" notat "\""))))))))
(defun coq-guess-or-ask-for-string (s &optional dontguess)
- "Asks for a coq identifier with message S.
+ "Asks for a Coq identifier with message S.
If DONTGUESS is non nil, propose a default value as follows:
-If region is active, propose its containt as default value.
+If region is active, propose its content as default value.
Otherwise propose identifier at point if any."
(let* ((guess
@@ -954,7 +954,7 @@ Otherwise propose identifier at point if any."
(defun coq-ask-do (ask do &optional dontguess postformatcmd wait)
"Ask for an ident and print the corresponding term.
-Add `'dont-show-when-silent' to supress show commands when running
+Add `'dont-show-when-silent' to suppress show commands when running
silent."
(let* ((cmd) (postform (if (eq postformatcmd nil) 'identity postformatcmd)))
(proof-shell-ready-prover)
@@ -1079,7 +1079,7 @@ This is specific to `coq-mode'."
(defun coq-Print (withprintingall)
"Ask for an ident and print the corresponding term.
-With flag Printing All if some prefix arg is given (C-u)."
+With flag Printing All if some prefix arg is given (\\[universal-argument])."
(interactive "P")
(if withprintingall
(coq-ask-do-show-all "Print" "Print")
@@ -1159,7 +1159,7 @@ This is specific to `coq-mode'."
(defun coq-Check (withprintingall)
"Ask for a term and print its type.
-With flag Printing All if some prefix arg is given (C-u)."
+With flag Printing All if some prefix arg is given (\\[universal-argument])."
(interactive "P")
(if withprintingall
(coq-ask-do-show-all "Check" "Check")
@@ -1191,7 +1191,7 @@ must be in locked region."
(defun coq-Show (withprintingall)
"Ask for a number I and show the Ith goal.
-Ask for a number I and show the ith current goal. With non-nil prefix
+Ask for a number I and show the ith current goal. With non-nil prefix
argument and not on the locked span, show the goal with flag
Printing All set."
; Disabled:
@@ -1236,7 +1236,7 @@ Printing All set."
;; FIXME: hopefully this will eventually become a non synchronized option and
;; we can remove this.
-;; This obeyx coq-auto-adapt-printing-width
+;; This obeys coq-auto-adapt-printing-width
(add-hook 'proof-assert-command-hook #'coq-adapt-printing-width)
(add-hook 'proof-retract-command-hook #'coq-reset-printing-width)
@@ -1579,7 +1579,7 @@ These are rehighlighted at each regeneration of goals buffer
using a hook in `proof-shell-handle-delayed-output-hook'.")
(defvar coq-highlighted-hyps-bg "gray"
- "background color for highlighted hyps.")
+ "Background color for highlighted hyps.")
(defun coq-highlight-hyp-aux (h)
@@ -1619,7 +1619,7 @@ use `coq-unhighlight-hyp' to unhighlight."
(defun coq-highlight-selected-hyps ()
"Highlight all hyps stored in `coq-highlighted-hyps'.
-This used in hook to rehilight hypothesis after goals buffer is
+This used in hook to rehighlight hypothesis after goals buffer is
updated."
(interactive)
(coq-highlight-hyps coq-highlighted-hyps))
@@ -1719,7 +1719,7 @@ using a hook in `proof-shell-handle-delayed-output-hook'.")
(defun coq-toggle-fold-hyp-at-mouse (event)
"Toggle hiding the hypothesis at mouse click.
-Used on hyptohesis overlays in goals buffer mainly."
+Used on hypothesis overlays in goals buffer mainly."
(interactive "e")
(save-excursion
(with-current-buffer proof-goals-buffer
@@ -1754,7 +1754,7 @@ Used on hyptohesis overlays in goals buffer mainly."
(defun coq-fold-hyp-aux (h)
"Fold hypothesis H's type from the context temporarily.
Displays \".......\" instead. This function relies on variable
-coq-hyps-positions. The hiding is cancelled as soon as the goals
+coq-hyps-positions. The hiding is canceled as soon as the goals
buffer is changed, consider using `coq-fold-hyp' if you want the
hiding to be maintain when scripting/undoing."
(let ((hyp-overlay (coq-find-hyp-overlay h)))
@@ -2052,17 +2052,17 @@ at `proof-assistant-settings-cmds' evaluation time.")
(defun coq-shell-mode-config ()
"Initialization of `coq-shell-mode' that runs in the `*coq*' buffer.
The interaction buffer with Coq, `*coq*', uses a major mode that
-is derived via `proof-shell-mode' from `scomint-mode'. This
+is derived via `proof-shell-mode' from `scomint-mode'. This
function runs as the body of `coq-shell-mode' when the `*coq*'
buffer is initialized, which happens when the Coq background
-process is started. This function intitalizes the Coq
+process is started. This function intitalizes the Coq
personalization of Proof General in the interaction buffer with
-Coq. At the end, this function calls `proof-shell-config-done',
+Coq. At the end, this function calls `proof-shell-config-done',
which initializes the Coq session, e.g., by sending
`proof-shell-init-cmd', respectively, `coq-shell-init-cmd' to Coq.
In normal interaction, the proof assistant is started because the
-user assert some commands. Therefore this function runs only
+user assert some commands. Therefore this function runs only
shortly before `proof-assert-command-hook', respectively,
`coq-adapt-printing-width'."
(setq
@@ -2223,7 +2223,7 @@ Return the empty string if the version of Coq < 8.10."
""))
(defun coq-diffs--setter (symbol new-value)
- ":set function fo `coq-diffs'.
+ ":set function to `coq-diffs'.
Set Diffs setting if Coq is running and has a version >= 8.10."
(set symbol new-value)
(if (proof-shell-available-p)
@@ -2234,7 +2234,7 @@ Set Diffs setting if Coq is running and has a version >= 8.10."
(proof-shell-invisible-command cmd)))))
(defcustom coq-diffs 'off
- "Controls Coq Diffs option"
+ "Controls Coq Diffs option."
:type '(radio
(const :tag "Don't show diffs" off)
(const :tag "Show diffs: only added" on)
@@ -2355,7 +2355,7 @@ This is the Coq incarnation of `proof-tree-find-undo-position'."
"Return the evar printing command for CMD as action list item.
Adds, among others, `'empty-action-list' to flags to avoid that
`coq-empty-action-list-command' adds a show command because it
-recognizes a change of a printing option. When the user quits the
+recognizes a change of a printing option. When the user quits the
proof tree display inside prooftree, then the evar command likely
runs as single command."
(proof-shell-action-list-item
@@ -2385,15 +2385,15 @@ Function for `proof-tree-display-stop-command'."
"Insert show-goal commands when running completely silent.
Coq specific function for `proof-tree-assistant-specific-urgent-action'.
When running completely silent, insert a show-goal command for commands
-comming from the user. Be careful to not insert show-goal commands for
+coming from the user. Be careful to not insert show-goal commands for
show-goal requests from prooftree or for the items inserted by this
-function. LAST-ITEM is the last proof-action item that has just been
-processed. This function is guaranteed to be called at a place where
+function. LAST-ITEM is the last proof-action item that has just been
+processed. This function is guaranteed to be called at a place where
`proof-action-list' can be directly manipulated.
When single stepping through a proof, this function inserts a second
show command, which is inserted before the one from
-`coq-show-goals-inside-proof'. One would of course be enough, but fixing
+`coq-show-goals-inside-proof'. One would of course be enough, but fixing
this would be difficult."
(let ((flags (nth 3 last-item)))
(unless (or (memq 'invisible flags)
@@ -2622,7 +2622,7 @@ Based on idea mentioned in Coq reference manual."
(defvar coq-auto-as-hack-hyp-name-regex
(concat "\\(" "induction\\|destruct" "\\)\\s-+\\(" coq-id-shy "\\)\\s-*\\.")
"Regexp of commands needing a hack to generate correct \"as\" close.
-tacitcs like destruct and induction reuse hypothesis names by
+tactics like destruct and induction reuse hypothesis names by
default, which makes the detection of new hypothesis incorrect.
the hack consists in adding the \"!\" modifier on the argument
destructed, so that it is left in the goal and the name cannot be
@@ -2631,7 +2631,7 @@ the whole tactic behaves correctly.
Warning: this makes the error messages (and location) wrong.")
(defun coq-hack-cmd-for-infoH (s)
- "return the tactic S hacked with infoH tactical."
+ "Return the tactic S hacked with infoH tactical."
(cond
;; We cannot rebuild the sub-patterns from the final goal, so ';' is not
;; supported. Only single tactics like destruct.
@@ -2673,8 +2673,8 @@ Warning: this makes the error messages (and location) wrong.")
"\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
- "Whether and how proofgeneral should insert \"Proof using\" suggestions.
-Suggestions are emitted by Coq at Qed time. The possible values
+ "Whether and how ProofGeneral should insert \"Proof using\" suggestions.
+Suggestions are emitted by Coq at Qed time. The possible values
of this variable are:
- 'always: always insert the suggested annotation
@@ -2684,29 +2684,28 @@ of this variable are:
coq-insert-suggested-dependency when point is on the proof
considered)
-- 'ask: asks the user each time. If yes then do as 'always, else
+- 'ask: asks the user each time. If yes then do as 'always, else
do as 'highlight
- 'never: ignore completely the suggestions.
Remarks and limitations:
- do not support nested proofs.
-- always use the *first* annotation suggested by coq.
+- always use the *first* annotation suggested by Coq.
- the proof is not replayed, which is consistent with the fact
that pg currently do not deal with async proofs.
- if there is already a \"Proof using\" annotation, then either it
- is correct and nothing happens, or it is incorrect and coq
+ is correct and nothing happens, or it is incorrect and Coq
generates an error. PG won't try to replace the erroneous
annotation in this case, but you can always go back, remove it
by hand, and let pg insert the good one.
-- instead of the menu you can do M-x coq-insert-suggested-dependency
- when point is on the proof considered.
-"
+- instead of the menu you can do \\[coq-insert-suggested-dependency]
+ when point is on the proof considered."
:type '(choice
(const :tag "Ask user" ask)
(const :tag "Always accept" always)
(const :tag "Higihlight" never)
- (const :tag "Ignore completely" ignore))
+ (const :tag "Ignore completely" ignore))
:group 'coq)
;; putting "Type" instead of nothing, otherwise Coq may fail if a "with"
@@ -2736,10 +2735,10 @@ annotation. See `proof-dependency-menu-system-specific'." )
"Regexp matching Coq \"Proof ....\" annotation (with no \"using\" annotation).
We suppose there is no \"using\" annotation, since Coq will fail
in this case and no suggestion can be added without replaying the
-script. Actually the only possible content iafter Proof is a
+script. Actually the only possible content after Proof is a
\"with annotation\".
The substring matched numbered 1 must start at the possible
-insertion point for the \"using\" annotation. ")
+insertion point for the \"using\" annotation.")
;; span is typically the whole theorem statement+proof span built after a save
@@ -2768,9 +2767,9 @@ insertion point for the \"using\" annotation. ")
(span-delete specialspan)))
(defun coq-find-Proof-command (start end)
- "look for a \"Proof\" command in span SPAN.
+ "Look for a \"Proof\" command in span SPAN.
-Return nil if not found. Set point to the end of \"Proof\"
+Return nil if not found. Set point to the end of \"Proof\"
otherwise and return position."
(goto-char start)
(let ((res t) found)
@@ -3090,14 +3089,14 @@ Completion is on a quasi-exhaustive list of Coq tacticals."
(defvar coq--error-location-regexp
"^Toplevel input, characters \\(?1:[0-9]+\\)-\\(?2:[0-9]+\\):\\(\n> [^\n]*\\)*\n"
- "A regexp to search the header of coq error locations.")
+ "A regexp to search the header of Coq error locations.")
;; I don't use proof-shell-last-output here since it is not always set to the
;; really last output (specially when a *tactic* gives an error) instead I go
;; directly to the response buffer. This allows also to clean the response
;; buffer (better to only scroll it?)
(defun coq-get-last-error-location (&optional parseresp clean)
- "Return location information on last error sent by coq.
+ "Return location information on last error sent by Coq.
Return a two elements list (POS LEN) if successful, nil otherwise.
@@ -3156,8 +3155,7 @@ If PARSERESP is nil, don't really parse response buffer but take the value of
If PARSERESP and CLEAN are non-nil, delete the error location from the response
buffer.
-Important: Coq gives char positions in bytes instead of chars.
-"
+Important: Coq gives char positions in bytes instead of chars."
(proof-with-current-buffer-if-exists proof-script-buffer
(let ((mtch (coq-get-last-error-location parseresp clean)))
(when mtch
@@ -3195,21 +3193,21 @@ Important: Coq gives char positions in bytes instead of chars.
If `coq-run-completely-silent' is set, add a Show command as
priority action, such that it will still be processed if the
generic machinery inside `proof-shell-filter' believes it has
-processed the last item from the action list. When Coq runs in
+processed the last item from the action list. When Coq runs in
silent mode, we need to update the goals precisely when
everything else from the action list has been processed.
The Show command is only added inside proofs and only if the last
-processed command was not a show command from this function. The
+processed command was not a show command from this function. The
action item flag `'dont-show-when-silent' is used for the latter.
KEEP-RESPONSE should be set if the last command produced some error or
-response that should be kept and shown to the user. If set, the flag
-`'keep-response' is added to the action item. When the show command is
+response that should be kept and shown to the user. If set, the flag
+`'keep-response' is added to the action item. When the show command is
processed in `proof-shell-handle-delayed-output', the flag causes that
the response buffer is not cleared and that in 2-pane mode the goals are
-not explicitely shown, see `pg-goals-display'. ON-ERROR should be set
-when there is some important message in the response buffer. In this
+not explicitly shown, see `pg-goals-display'. ON-ERROR should be set
+when there is some important message in the response buffer. In this
case `'no-response-display' is added to the flags such that a \"no more
goals\" reply to the Show command does not overwrite the response
buffer.
@@ -3229,7 +3227,7 @@ Do nothing if `coq-run-completely-silent' is disabled."
"Update goals after error.
This function is intended for
`proof-shell-handle-error-or-interrupt-hook' to update the goals
-buffer after an error has been detected. See also
+buffer after an error has been detected. See also
`coq-show-goals-inside-proof'."
(coq-show-goals-inside-proof t t))
@@ -3238,8 +3236,8 @@ buffer after an error has been detected. See also
This function is intended for
`proof-shell-handle-delayed-output-hook' to update the goals
buffer after the last command has been processed and no error has
-been detected. Take care to keep the response buffer visible if
-the last command was a Search, a Check or something similar. See
+been detected. Take care to keep the response buffer visible if
+the last command was a Search, a Check or something similar. See
also `coq-show-goals-inside-proof'."
(coq-show-goals-inside-proof (eq proof-shell-last-output-kind 'response) nil))
@@ -3338,7 +3336,7 @@ number of hypothesis displayed, without hiding the goal"
(defun coq-clean-goals-outside-proof ()
"Clear goals buffer outside proofs.
This function ensures that the goals buffer is reset after Qed or
-Admitted. This function is for
+Admitted. This function is for
`proof-shell-handle-delayed-output-hook'."
(when (or (not coq-last-but-one-proofstack)
(proof-string-match coq-shell-proof-completed-regexp
@@ -3434,7 +3432,7 @@ Only when three-buffer-mode is enabled."
;; TODO: Have the same for other commands, but with insertion at all.
(defcustom coq-double-hit-enable nil
- "* Experimental: Whether or not double hit should be enabled in coq mode.
+ "* Experimental: Whether or not double hit should be enabled in Coq mode.
A double hit is performed by pressing twice a key quickly. If
this variable is not nil, then 1) it means that electric
terminator is off and 2) a double hit on the terminator act as
@@ -3446,7 +3444,7 @@ the usual electric terminator. See `proof-electric-terminator'."
(defvar coq-double-hit-hot-key "."
"The key used for double hit electric terminator.
-By default this is the coq terminator \".\" key.
+By default this is the Coq terminator \".\" key.
For example one can do this:
\(setq coq-double-hit-hot-key (kbd \";\"))
@@ -3488,7 +3486,7 @@ This is an advice to pg `proof-electric-terminator-enable' function."
(ad-activate 'proof-electric-terminator-enable)
(defvar coq-double-hit-delay 0.25
- "The maximum delay between the two hit of a double hit in coq/proofgeneral.")
+ "The maximum delay between the two hit of a double hit in Coq/ProofGeneral.")
(defvar coq-double-hit-timer nil
"The timer used to watch for double hits.")
@@ -3558,12 +3556,12 @@ correct in the new scripting buffer."
(add-hook 'proof-deactivate-scripting-hook #'coq-kill-proof-shell t)
(defcustom coq-kill-coq-on-opam-switch t
- "If t kill coq when the opam switch changes (requires `opam-switch-mode').
+ "If t kill Coq when the opam switch changes (requires `opam-switch-mode').
When `opam-switch-mode' is loaded and the user changes the opam switch
-through `opam-switch-mode' then this option controls whether the coq
+through `opam-switch-mode' then this option controls whether the Coq
background process (the proof shell) is killed such that the next
assert command starts a new proof shell, probably using a
-different coq version from a different opam switch.
+different Coq version from a different opam switch.
See https://github.com/ProofGeneral/opam-switch-mode for `opam-switch-mode'"
:type 'boolean
@@ -3574,10 +3572,10 @@ See https://github.com/ProofGeneral/opam-switch-mode for `opam-switch-mode'"
"Kill proof shell when the opam switch changes (requires `opam-switch-mode').
This function is for the `opam-switch-mode' hook
`opam-switch-change-opam-switch-hook', which runs when the user
-changes the opam switch through `opam-switch-mode'. If
+changes the opam switch through `opam-switch-mode'. If
`coq-kill-coq-on-opam-switch' is t, then the proof shell is
killed such that the next assert starts a new proof shell, using
-coq from the new opam switch."
+Coq from the new opam switch."
(when (and coq-kill-coq-on-opam-switch proof-script-buffer)
(coq-kill-proof-shell)))
diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi
index 05327433c..6a5a7328c 100644
--- a/doc/PG-adapting.texi
+++ b/doc/PG-adapting.texi
@@ -518,7 +518,7 @@ Command to display the context in proof assistant.
@c TEXI DOCSTRING MAGIC: proof-info-command
@defvar proof-info-command
Command to ask for help or information in the proof assistant.@*
-String or fn. If a string, the command to use.
+String or function. If a string, the command to use.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-showproof-command
@@ -527,21 +527,21 @@ Command to display proof state in proof assistant.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-goal-command
@defvar proof-goal-command
-Command to set a goal in the proof assistant. String or fn.@*
+Command to set a goal in the proof assistant. String or function.@*
If a string, the format character @samp{%s} will be replaced by the
goal string.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-save-command
@defvar proof-save-command
-Command to save a proved theorem in the proof assistant. String or fn.@*
+Command to save a proved theorem in the proof assistant. String or function.@*
If a string, the format character @samp{%s} will be replaced by the
theorem name.
If a function, it should return the command string to insert.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-find-theorems-command
@defvar proof-find-theorems-command
-Command to search for a theorem containing a given term. String or fn.@*
+Command to search for a theorem containing a given term. String or function.@*
If a string, the format character @samp{%s} will be replaced by the term.
If a function, it should return the command string to send.
@end defvar
@@ -1185,9 +1185,9 @@ configured.
@c TEXI DOCSTRING MAGIC: proof-omit-proofs-configured
@defvar proof-omit-proofs-configured
-t if the omit proofs feature has been configured by the proof assitant.@*
+Non-nil if the omit proofs feature has been configured by the proof assistant.@*
See also @samp{@code{proof-omit-proofs-option}} or the Proof General manual
-for a description of the feature. This option can only be set, if
+for a description of the feature. This option can only be set, if
all of @samp{@code{proof-script-proof-start-regexp}},
@samp{@code{proof-script-proof-end-regexp}},
@samp{@code{proof-script-definition-end-regexp}} and
@@ -1201,7 +1201,7 @@ commands in the source following a match of
@samp{@code{proof-script-proof-start-regexp}} up to and including the next
match of @samp{@code{proof-script-proof-end-regexp}}, are omitted (not send
to the proof assistant) and replaced by
-@samp{@code{proof-script-proof-admit-command}}. If a match for
+@samp{@code{proof-script-proof-admit-command}}. If a match for
@samp{@code{proof-script-definition-end-regexp}} is found while searching
forward for the proof end or if
@samp{@code{proof-script-cmd-prevents-proof-omission}} recognizes a proof
@@ -1212,7 +1212,7 @@ to and including the match of
and not omitted, thus all these proof commands _are_ sent to the
proof assistant.
-The feature does not work for nested proofs. If a match for
+The feature does not work for nested proofs. If a match for
@samp{@code{proof-script-proof-start-regexp}} is found before the next match
for @samp{@code{proof-script-proof-end-regexp}} or
@samp{@code{proof-script-definition-end-regexp}}, the search for opaque
@@ -1252,11 +1252,11 @@ Proof command to be inserted instead of omitted proofs.
@defvar proof-script-cmd-prevents-proof-omission
Optional predicate to match commands that prevent omitting the current proof.@*
If set, this option should contain a function that takes a proof
-command (as string) as argument and returns t or nil. If set, the
+command (as string) as argument and returns t or nil. If set, the
function is called on every proof command inside a proof while
-scanning for proofs to omit. The predicate should return t if the
-command has effects ouside the proof, potentially breaking the
-script if the current proof is omitted. If the predicate returns
+scanning for proofs to omit. The predicate should return t if the
+command has effects outside the proof, potentially breaking the
+script if the current proof is omitted. If the predicate returns
t, the proof is considered to be not opaque and thus not omitted.
@end defvar
@@ -1265,9 +1265,9 @@ t, the proof is considered to be not opaque and thus not omitted.
Optional regexp for commands that prevent omitting the next proof.@*
If set, this option should contain a regular expression that
matches proof-script commands that prevent the omission of proofs
-dirctly following this command. When scanning the newly asserted
+directly following this command. When scanning the newly asserted
region for proofs to omit, every proof-script command outside
-proofs is matched against this regexp. If it matches and the next
+proofs is matched against this regexp. If it matches and the next
command matches @samp{@code{proof-script-proof-start-regexp}} this following
proof will not be omitted.
@@ -1304,10 +1304,10 @@ following settings must be configured.
@c TEXI DOCSTRING MAGIC: proof-get-proof-info-fn
@defvar proof-get-proof-info-fn
Return proof name and state number for @samp{@code{proof-check-proofs}}.@*
-Proof assistant specific function for @samp{@code{proof-check-proofs}}. This
+Proof assistant specific function for @samp{@code{proof-check-proofs}}. This
function takes no arguments, it is called after completely
processing the proof script up to a certain point (including all
-callbacks in spans). It must return a list, which contains, in
+callbacks in spans). It must return a list, which contains, in
the following order:
* the current state number (as positive integer)
@@ -1327,7 +1327,7 @@ should be a no-op.
@defvar proof-retract-command-fn
Function for retract command to a certain state.@*
This function takes a state as argument as returned by
-@samp{@code{proof-get-proof-info-fn}}. It should return a command that brings
+@samp{@code{proof-get-proof-info-fn}}. It should return a command that brings
the proof assistant back to the same state.
@end defvar
@@ -1335,11 +1335,11 @@ the proof assistant back to the same state.
@defvar proof-omit-cheating-regexp
Regular expression matching proof closing commands for incomplete proofs.@*
If set, this regular expression is applied to the last command of
-opaque proofs. If it matches the proofs counts as invalid for the
-proof-status statistics and annotation feature. For Coq this is
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
used to mark Admitted proofs as invalid.
-This option can be left at @samp{nil}.
+This option can be left at nil.
@end defvar
@@ -1568,7 +1568,7 @@ If @samp{@code{proof-terminal-string}} is nil, this has no effect.
The command for configuring the proof process to gain synchronization.@*
This command is sent before Proof General's synchronization
mechanism is engaged, to allow customization inside the process
-to help gain syncrhonization (e.g. engaging special markup).
+to help gain synchronization (e.g. engaging special markup).
It is better to configure the proof assistant for this purpose
via command line options if possible, in which case this variable
@@ -1590,7 +1590,7 @@ See also @samp{@code{proof-shell-pre-sync-init-cmd}}.
@c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd
@defvar proof-shell-restart-cmd
-A command for re-initialising the proof process.
+A command for re-initializing the proof process.
@end defvar
@c TEXI DOCSTRING MAGIC: proof-shell-quit-cmd
@@ -1737,7 +1737,7 @@ are normally the ones of interest:
@code{'proof-done-advancing} A "forward" scripting command
@code{'proof-done-retracting} A "backward" scripting command
@code{'proof-done-invisible} A non-scripting command
- @code{'proof-shell-set-silent} Indicates prover output has been surpressed
+ @code{'proof-shell-set-silent} Indicates prover output has been suppressed
@code{'proof-shell-clear-silent} Indicates prover output has been restored
@code{'init-cmd} Early initialization command sent to prover
@end lisp
@@ -1858,7 +1858,7 @@ command, depending on whether the prover supports nested proofs or not.
Regexp matching the start of the proof state output.@*
This is an important setting. Output between @samp{@code{proof-shell-start-goals-regexp}}
and @samp{@code{proof-shell-end-goals-regexp}} will be pasted into the goals buffer
-and possibly analysed further for proof-by-pointing markup.
+and possibly analyzed further for proof-by-pointing markup.
If it is left as nil, the goals buffer will not be used.
The goals display starts at the beginning of the match on this
@@ -1915,7 +1915,7 @@ parsing later. Note that this affects processing of output which is
ordinarily accumulated: output which appears before the eager annotation
start will be discarded.
-The start/end annotations can be used to hilight the output, but
+The start/end annotations can be used to highlight the output, but
are stripped from display of the message in the minibuffer.
It is useful to recognize (starts of) warnings or file-reading messages
@@ -2169,7 +2169,7 @@ before returning to the top level.
@c TEXI DOCSTRING MAGIC: proof-shell-handle-output-system-specific
@defvar proof-shell-handle-output-system-specific
Set this variable to handle system specific output.@*
-Errors and interrupts are recognised in the function
+Errors and interrupts are recognized in the function
@samp{@code{proof-shell-handle-immediate-output}}. Later output is
handled by @samp{@code{proof-shell-handle-delayed-output}}, which
displays messages to the user in @strong{goals} and @strong{response}
@@ -2284,7 +2284,7 @@ Proof General.
@defvar proof-splash-contents
Evaluated to configure splash screen displayed when entering Proof General.@*
A list of the screen contents. If an element is a string or an image
-specifier, it is displayed centred on the window on its own line.
+specifier, it is displayed centered on the window on its own line.
If it is nil, a new line is inserted.
@end defvar
@@ -2614,7 +2614,7 @@ the current restriction, and must return the final value of (@code{point-max}).
@c TEXI DOCSTRING MAGIC: pg-after-fontify-output-hook
@defvar pg-after-fontify-output-hook
-This hook is called before fonfitying a region in an output buffer.@*
+This hook is called before fontifying a region in an output buffer.@*
[This hook is presently only used by Isabelle].
@end defvar
@@ -2943,12 +2943,12 @@ speed, the amount of urgent code should be kept small.
@defun proof-tree-urgent-action last-item
Urgent actions for proof-tree display.@*
This is the second entry point of the Proof General prooftree support,
-see also @samp{@code{proof-tree-handle-delayed-output}}. Call
+see also @samp{@code{proof-tree-handle-delayed-output}}. Call
@samp{@code{proof-tree-check-proof-finish}} to delay processing the queue region at
the end of a proof until all show-goal commands from prooftree have been
-processed. Do also call @samp{@code{proof-tree-assistant-specific-urgent-action}},
+processed. Do also call @samp{@code{proof-tree-assistant-specific-urgent-action}},
which appropriately inserts show-goal commands if Coq is running
-completely silent. @var{last-item} is the last proof-action item that has just
+completely silent. @var{last-item} is the last proof-action item that has just
been processed.
When the proof-tree display is active, this function is called from
@@ -2974,7 +2974,7 @@ assistant is already busy with the next item from
@defun proof-tree-handle-delayed-output old-proof-marker cmd flags _span
Process delayed output for prooftree.@*
This function is the main entry point of the Proof General prooftree
-support, but see also @samp{@code{proof-tree-urgent-action}}. It examines the
+support, but see also @samp{@code{proof-tree-urgent-action}}. It examines the
delayed output in order to take appropriate actions and maintains the
internal state.
@@ -3634,7 +3634,7 @@ important one is @code{proof-init-segmentation}.
@c TEXI DOCSTRING MAGIC: proof-init-segmentation
@defun proof-init-segmentation
-Initialise the queue and locked spans in a proof script buffer.@*
+Initialize the queue and locked spans in a proof script buffer.@*
Allocate spans if need be. The spans are detached from the
buffer, so the regions are made empty by this function.
Also clear list of script portions.
@@ -3968,7 +3968,7 @@ bother the user. They may include
show command when running silent.
@end lisp
Note that @code{'invisible} does not imply any of the others. If flags
-are non-empty, interactive cues will be surpressed. (E.g.,
+are non-empty, interactive cues will be suppressed. (E.g.,
printing hints).
See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-exec-loop}}.
@@ -3979,7 +3979,7 @@ See the functions @samp{@code{proof-start-queue}} and @samp{@code{proof-shell-ex
Position of end of second last input inside delayed callbacks.@*
When callbacks of action items are processed, @samp{@code{proof-marker}} has already
been advanced to the end of the next input that the proof assistant
-processes in parallel with the callback. This variable permits the
+processes in parallel with the callback. This variable permits the
callback to access the end of the input belonging to its action-list
item and then process the complete output that the proof assistant has
sent.
@@ -4017,7 +4017,7 @@ background compilation finishes. Then those items are put into
@defvar pg-subterm-anns-use-stack
Choice of syntax tree encoding for terms.
-If nil, prover is expected to make no optimisations.
+If nil, prover is expected to make no optimizations.
If non-nil, the pretty printer of the prover only reports local changes.
For Coq 6.2, use t.
@end defvar
@@ -4028,7 +4028,7 @@ buffer and the associated buffers.
@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn Command proof-shell-start
-Initialise a shell-like buffer for a proof assistant.@*
+Initialize a shell-like buffer for a proof assistant.@*
Does nothing if proof assistant is already running.
Also generates goal and response buffers.
@@ -4358,7 +4358,7 @@ will also be displayed in the response buffer.
For example, if @var{output} has this form:
@lisp
- @var{messsage-1}
+ @var{message-1}
@var{goals-1}
@var{message-2}
@var{goals-2}
@@ -4488,7 +4488,7 @@ entry point, @samp{@code{proof-shell-filter}} against such parallel,
overlapping calls.
The argument @var{str-do-not-use} contains the most recent output, but
-is discarded. @samp{@code{proof-shell-filter}} collects the output from
+is discarded. @samp{@code{proof-shell-filter}} collects the output from
@samp{@code{proof-shell-buffer}} (where it is inserted by
@samp{@code{scomint-output-filter}}), relieving this function from the task
to buffer the output that arrives during parallel, overlapping
diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi
index 19b7770c6..197fc9181 100644
--- a/doc/ProofGeneral.texi
+++ b/doc/ProofGeneral.texi
@@ -1785,7 +1785,7 @@ does not. As with any Emacs command, you can invoke these with
@c TEXI DOCSTRING MAGIC: proof-shell-start
@deffn Command proof-shell-start
-Initialise a shell-like buffer for a proof assistant.@*
+Initialize a shell-like buffer for a proof assistant.@*
Does nothing if proof assistant is already running.
Also generates goal and response buffers.
@@ -2286,7 +2286,7 @@ only work for Coq.
Generate an overview about valid and invalid proofs.@*
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid. Note that
+whether their proof scripts are valid or invalid. Note that
proofs closed with a cheating command (see
@samp{@code{proof-omit-cheating-regexp}}), i.e., Admitted for Coq, count as
invalid.
@@ -2298,20 +2298,20 @@ the most interesting or challenging point instead of on the first
invalid proof.
Argument @var{tap}, which can be set by a prefix argument, controls the
-form of the generated overview. Nil, without prefix, gives an
+form of the generated overview. Nil, without prefix, gives an
human readable overview, otherwise it's test anything
-protocol (@var{tap}). Argument @var{batch} controls where the overview goes
-to. If nil, or in an interactive call, the overview appears in
-@samp{@code{proof-check-report-buffer}}. If @var{batch} is a string, it should be a
-filename to write the overview to. Otherwise the overview is
+protocol (@var{tap}). Argument @var{batch} controls where the overview goes
+to. If nil, or in an interactive call, the overview appears in
+@samp{@code{proof-check-report-buffer}}. If @var{batch} is a string, it should be a
+filename to write the overview to. Otherwise the overview is
output via @samp{message} such that it appears on stdout when this
command runs in batch mode.
In the same way as the omit-proofs feature, this command only
-tolerates errors inside scripts of opaque proofs. Any other error
-is reported to the user without generating an overview. The
+tolerates errors inside scripts of opaque proofs. Any other error
+is reported to the user without generating an overview. The
overview only contains those names of theorems whose proof
-scripts are classified as opaque by the omit-proofs feature. For
+scripts are classified as opaque by the omit-proofs feature. For
Coq for instance, among others, proof scripts terminated with
@code{'Defined'} are not opaque and do not appear in the generated
overview.
@@ -2324,14 +2324,14 @@ instance by asserting all require commands beforehand.
@c TEXI DOCSTRING MAGIC: proof-check-annotate
@deffn Command proof-check-annotate annotate-passing &optional save-buffer
Annotate failing proofs in current buffer with a "@var{fail}" comment.@*
-This function modifies the current buffer in place. Use with
+This function modifies the current buffer in place. Use with
care!
Similarly to @samp{@code{proof-check-report}}, check all opaque proofs in the
-current buffer. Instead of generating a report, failing proofs
-are annotated with "@var{fail}" in a comment. Existing "@var{pass}" or
+current buffer. Instead of generating a report, failing proofs
+are annotated with "@var{fail}" in a comment. Existing "@var{pass}" or
"@var{fail}" comments (e.g., from a previous run) are deleted
-together with the surrounding white space. With prefix argument
+together with the surrounding white space. With prefix argument
(or when @var{annotate-passing} is non-nil) also passing proofs are
annotated with a "@var{pass}" comment. Pass and fail comments can be
placed at the last or second last statement before the opaque
@@ -3797,7 +3797,7 @@ you want to send already has a terminator character, you don't
need to delete the terminator character first. Just press the
terminator somewhere nearby. Electric!
-The default value is @code{nil}.
+The default value is @code{#[128 "\304\301\"\304\300\"\210\207" ['coq-unset-double-hit-advice nil :after nil apply] 5 advice]}.
@end defopt
@c TEXI DOCSTRING MAGIC: proof-next-command-insert-space
@@ -3851,7 +3851,7 @@ The default value is @code{t}.
@defvar proof-omit-proofs-option
Set to t to omit complete opaque proofs for speed reasons.@*
When t, complete opaque proofs in the asserted region are not
-sent to the proof assistant (and thus not checked). For files
+sent to the proof assistant (and thus not checked). For files
with big proofs this can drastically reduce the processing time
for the asserted region at the cost of not checking the proofs.
For partial and non-opaque proofs in the asserted region all
@@ -3952,7 +3952,7 @@ One of the symbols: @code{'locked}, @code{'follow}, @code{'followdown}, @code{'i
If @code{'locked}, point sticks to the end of the locked region.
If @code{'follow}, point moves just when needed to display the locked region end.
-If @code{'followdown}, point if necessary to stay in writeable region
+If @code{'followdown}, point if necessary to stay in writable region
If @code{'ignore}, point is never moved after movement commands or on errors.
If you choose @code{'ignore}, you can find the end of the locked using
@@ -4046,11 +4046,11 @@ Face for locked region of proof script (processed commands).
@c TEXI DOCSTRING MAGIC: proof-script-sticky-error-face
@deffn Face proof-script-sticky-error-face
-Proof General face for marking an error in the proof script.
+Proof General face for marking an error in the proof script.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-script-highlight-error-face
@deffn Face proof-script-highlight-error-face
-Proof General face for highlighting an error in the proof script.
+Proof General face for highlighting an error in the proof script.
@end deffn
@c TEXI DOCSTRING MAGIC: proof-mouse-highlight-face
@deffn Face proof-mouse-highlight-face
@@ -4531,30 +4531,29 @@ Variable containing the function detecting a project file.
See its default value @samp{@code{coq--default-project-find-file}} for an example.
The function takes one argument, the name of a directory, and returns
-the name of a coq/rocq project file it contains if there is one. Return
+the name of a Coq/Rocq project file it contains if there is one. Return
nil otherwise.
-This is used to detect the coq project file (using
-@samp{@code{locate-dominating-file}}). By default we accept _CoqProject and
-_RocqProject (and any case-variant of these) without checking coq/rocq
-version. If you want something smarter please redefine
+This is used to detect the Coq project file (using
+@samp{@code{locate-dominating-file}}). By default we accept _CoqProject and
+_RocqProject (and any case-variant of these) without checking Coq/Rocq
+version. If you want something smarter please redefine
@samp{@code{coq-project-filename}} directly by using:
(setq @code{coq-project-filename} #'my-own-predicate)
-About the coq/rocq project file (cf. Coq documentation on project files
+About the Coq/Rocq project file (cf. Coq documentation on project files
and "makefile generation"):
-The coq project file of a coq development should contain the arguments
-given to coq_makefile. In particular it contains the -I and -R
+The Coq project file of a Coq development should contain the arguments
+given to Coq_makefile. In particular it contains the -I and -R
options (preferably one per line). If @samp{coq-use-coqproject} is
t (default) the content of this file will be used by Proof General to
infer the @samp{@code{coq-load-path}} and the @samp{@code{coq-prog-args}} variables that set the
coqtop invocation by Proof General. This is now the recommended way of
configuring the coqtop invocation. Local file variables may still be
-used to override the coq project file's configuration. .dir-locals.el
+used to override the Coq project file's configuration. .dir-locals.el
files also work and override project file settings.
-
@end defvar
@@ -5021,8 +5020,8 @@ This option can be set/reset via menu
@c TEXI DOCSTRING MAGIC: coq-compile-auto-save
@defvar coq-compile-auto-save
Buffers to save before checking dependencies for compilation.@*
-There are two orthogonal choices: Firstly one can save all or only the coq
-buffers, where coq buffers means all buffers in coq mode except the current
+There are two orthogonal choices: Firstly one can save all or only the Coq
+buffers, where Coq buffers means all buffers in Coq mode except the current
buffer. Secondly, Emacs can ask about each such buffer or save all of them
unconditionally.
@@ -5177,7 +5176,7 @@ configure these things with the following options.
@c TEXI DOCSTRING MAGIC: coq-load-path
@defvar coq-load-path
-Non-standard coq library load path.@*
+Non-standard Coq library load path.@*
This list specifies the LoadPath extension for coqdep, coqc and
coqtop. Usually, the elements of this list are strings (for
"-I") or lists of two strings (for "-R" dir path and
@@ -5187,7 +5186,7 @@ The possible forms of elements of this list correspond to the 4
forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be
@lisp
- A list of the form @samp{(}ocamlimport dir)', specifying (in 8.5) a
- directory to be added to ocaml path (@samp{-I}).
+ directory to be added to Ocaml path (@samp{-I}).
- A list of the form @samp{(}rec dir path)' (where dir and path are
strings) specifying a directory to be recursively mapped to the
logical path @samp{path} (@samp{-R dir path}).
@@ -5205,11 +5204,11 @@ the form @samp{(dir path)} are interpreted as @samp{(rec dir path)}.
A plain string maps to -Q ... "" in 8.5, and -I ... in 8.4.
Under normal circumstances this list does not need to
-contain the coq standard library or "." for the current
+contain the Coq standard library or "." for the current
directory (see @samp{@code{coq-load-path-include-current}}).
-@var{warning}: if you use coq <= 8.4, the meaning of these options is
-not the same (-I is for coq path).
+@var{warning}: if you use Coq <= 8.4, the meaning of these options is
+not the same (-I is for Coq path).
@end defvar
@@ -5237,7 +5236,7 @@ List of regular expressions for directories in which ProofGeneral
should not compile modules. If a library file name matches one
of the regular expressions in this list then ProofGeneral does
neither compile this file nor check its dependencies for
-compilation. It makes sense to include non-standard coq library
+compilation. It makes sense to include non-standard Coq library
directories here if they are not changed and if they are so big
that dependency checking takes noticeable time. The regular
expressions in here are always matched against the .vo file name,
@@ -5626,12 +5625,12 @@ is killed when changing the opam switch through
@c TEXI DOCSTRING MAGIC: coq-kill-coq-on-opam-switch
@defvar coq-kill-coq-on-opam-switch
-If t kill coq when the opam switch changes (requires @samp{opam-switch-mode}).@*
+If t kill Coq when the opam switch changes (requires @samp{opam-switch-mode}).@*
When @samp{opam-switch-mode} is loaded and the user changes the opam switch
-through @samp{opam-switch-mode} then this option controls whether the coq
+through @samp{opam-switch-mode} then this option controls whether the Coq
background process (the proof shell) is killed such that the next
assert command starts a new proof shell, probably using a
-different coq version from a different opam switch.
+different Coq version from a different opam switch.
See https://github.com/ProofGeneral/opam-switch-mode for @samp{opam-switch-mode}
@end defvar
diff --git a/generic/pg-assoc.el b/generic/pg-assoc.el
index d67177302..a76408177 100644
--- a/generic/pg-assoc.el
+++ b/generic/pg-assoc.el
@@ -25,7 +25,7 @@
(require 'proof-utils)
(define-derived-mode proof-universal-keys-only-mode fundamental-mode
- proof-general-name "Universal keymaps only"
+ proof-general-name "Universal keymaps only."
;; Doesn't seem to supress TAB, RET
(suppress-keymap proof-universal-keys-only-mode-map 'all)
(proof-define-keys proof-universal-keys-only-mode-map
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 2bb1d05bd..2fefc0bf9 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -168,7 +168,7 @@
(defun pg-autotest-test-process-wholefile (file)
"Load FILE and script in one go.
-An error is signalled if scripting doesn't completely the whole buffer."
+An error is signaled if scripting doesn't completely the whole buffer."
(pg-autotest-find-file-restart file)
(proof-process-buffer)
(proof-shell-wait)
@@ -176,7 +176,7 @@ An error is signalled if scripting doesn't completely the whole buffer."
(defun pg-autotest-test-script-wholefile (file)
"Process FILE line-by-line, using `proof-shell-wait'.
-An error is signalled if scripting doesn't complete."
+An error is signaled if scripting doesn't complete."
(pg-autotest-find-file-restart file)
(save-excursion
(let ((making-progress t) last-locked-end)
diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 0bba1553c..d3e872855 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -72,7 +72,7 @@ May enable proof-by-pointing or similar features.
;;
;;;###autoload
(defun proof-goals-config-done ()
- "Initialise the goals buffer after the child has been configured."
+ "Initialize the goals buffer after the child has been configured."
(setq font-lock-defaults '(proof-goals-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -94,7 +94,7 @@ so the response buffer should not be cleared.
IF NODISPLAY is non-nil, do not display the goals buffer in some
window (but the goals buffer is updated as described above and
-any window currently showing it will keep it). In two-pane mode,
+any window currently showing it will keep it). In two-pane mode,
NODISPLAY has the effect that the goals are updated but the
response buffer is displayed."
;; Response buffer may be out of date. It may contain (error)
diff --git a/generic/pg-pbrpm.el b/generic/pg-pbrpm.el
index dd34965bf..9927b0839 100644
--- a/generic/pg-pbrpm.el
+++ b/generic/pg-pbrpm.el
@@ -129,14 +129,14 @@ Matches the region to be returned.")
It stores, in the variable ‘pg-pbrpm-goal-description’, a list with shape
-(start-goal end-goal goal-name start-concl hyps ...) with 5 elements per goal:
+\(start-goal end-goal goal-name start-concl hyps ...) with 5 elements per goal:
start-goal: the position of the first char of the goal
end-goal: the position of the last char of the goal
goal-name: the goal name (or number)
start-concl: the position of first char of the conclusion of the goal
hyps: the list of hypothesis with the shape:
-(start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elements per hypothesis:
+\(start-hyp start-hyp-text end-hyp hyp-name ...) with 4 elements per hypothesis:
start-hyp: the position of the first char of the hyp (including its name)
start-hyp-text: the position of the first char of the hyp formula (no name)
end-hyp: the position of the last char of the hypothesis
@@ -206,7 +206,7 @@ It stores, in the variable ‘pg-pbrpm-goal-description’, a list with shape
(defun pg-pbrpm-build-menu (event start end)
"Build a Proof By Rules pop-up menu.
Depends on the state of the proof, the event and a selected region
-(between the start and end markers).
+\(between the start and end markers).
The prover command is processed via pg-pbrpm-run-command."
;; first, run the prover specific (name, rule)'s list generator
(let ((click-info (pg-pbrpm-process-click event start end))) ; retrieve click informations
@@ -417,7 +417,7 @@ See `pg-pbrpm-get-pos-info'."
nil)))
(defun pg-pbrpm-auto-select-around-point ()
- "Extract some text arround point, according to `pg-pbrpm-auto-select-regexp'.
+ "Extract some text around point, according to `pg-pbrpm-auto-select-regexp'.
If no match found, return the empty string."
(save-excursion
(let ((pos (point)))
@@ -562,7 +562,7 @@ SPAN is a span covering the selected region."
(mapcar (lambda (span) (pg-pbrpm-process-region span)) pg-pbrpm-regions-list))
(defun pg-pbrpm-region-expression (buffer start end)
- "Valid parenthesis'd expression."
+ "Valid parenthesized expression."
;; an expression is valid if it has as many left paren' as right paren'
(with-current-buffer buffer
(buffer-substring start end)))
@@ -600,4 +600,5 @@ SPAN is a span covering the selected region."
(define-key pg-span-context-menu-keymap [(control button3)] 'pg-span-context-menu)))
(provide 'pg-pbrpm)
-;;; pg-pbrpm ends here
+
+;;; pg-pbrpm.el ends here
diff --git a/generic/pg-pgip.el b/generic/pg-pgip.el
index 0954b5049..ccfd4ef23 100644
--- a/generic/pg-pgip.el
+++ b/generic/pg-pgip.el
@@ -27,7 +27,7 @@
;;
;; TODO NEXT:
;; -- completion command for completion tables
-;; -- parsescript input/outputs
+;; -- parse script input/outputs
;; -- guiconfig, some parts of
;; -- support fully native PGIP mode
;;
@@ -384,7 +384,7 @@ Return a symbol representing the PGIP command processed, or nil."
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defvar pg-pgip-srcids nil
- "Association list of srcrds to (buffer file) lists")
+ "Association list of srcrds to (buffer file) lists.")
;; FIXME: right action?
(defun pg-pgip-process-newfile (node)
@@ -498,7 +498,7 @@ Also sets local proverid and srcid variables for buffer."
((eq (car-safe type) 'choice)
(pg-pgip-default-for (car-safe (cdr-safe type))))
(t
- (pg-pgip-error "pg-pgip-default-for: unrecognized type passed in"))))
+ (pg-pgip-error "pg-pgip-default-for: Unrecognized type passed in"))))
(defun pg-pgip-subst-for (type)
"Return a substitution string for type TYPE."
@@ -530,7 +530,7 @@ Also sets local proverid and srcid variables for buffer."
((eq (car-safe type) 'choice)
(pg-pgip-interpret-choice (cdr type) value))
(t
- (pg-pgip-error "pg-pgip-interpret-value: unkown type %s" type))))
+ (pg-pgip-error "pg-pgip-interpret-value: Unknown type %s" type))))
(defun pg-pgip-interpret-choice (choices value)
;; Untagged union types: test for value in each type in turn.
@@ -555,7 +555,7 @@ Also sets local proverid and srcid variables for buffer."
(setq choices (cdr choices)))
(or res
(pg-pgip-error
- "pg-pgip-interpret-choice: mismatching value %s for choices %s"
+ "pg-pgip-interpret-choice: Mismatching value %s for choices %s"
value choices))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -566,7 +566,7 @@ Also sets local proverid and srcid variables for buffer."
(defun pg-pgip-string-of-command (pgip &optional refseq refid otherclass)
"Convert XML node PGIP or string into a command string to send to the prover.
This wraps the node in a packet with appropriate attributes.
-See `pg-pgip-assemble-packet' "
+See `pg-pgip-assemble-packet'"
(let ((wrappedpgip
(pg-xml-string-of
(list (pg-pgip-assemble-packet (list pgip) refseq refid otherclass)))))
@@ -590,9 +590,9 @@ See `pg-pgip-assemble-packet' "
"PGIP Identifier for this Emacs Proof General component.")
(defvar pg-pgip-refseq nil
- "The sequence number of the received message this reply refers to")
+ "The sequence number of the received message this reply refers to.")
(defvar pg-pgip-refid nil
- "The identity of the component this message is being sent to")
+ "The identity of the component this message is being sent to.")
(defvar pg-pgip-seq 0 "Sequence number of messages sent out.")
@@ -655,7 +655,7 @@ the prover. For remaining optional args, see doc of
(defun pg-pgip-reset ()
- "Reset state of the PGIP module"
+ "Reset state of the PGIP module."
(setq pg-pgip-refseq nil
pg-pgip-refid nil
pg-pgip-last-seen-id nil
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 339605ea4..8a67a0785 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -32,7 +32,7 @@
(require 'span)
(defvar pg-insert-text-function #'insert
- "hook for coq diffs highlighting routine")
+ "Hook for Coq diffs highlighting routine.")
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -51,7 +51,7 @@
;;;###autoload
(define-derived-mode proof-response-mode proof-universal-keys-only-mode
- "PGResp" "Responses from Proof Assistant"
+ "PGResp" "Responses from Proof Assistant."
(setq proof-buffer-type 'response)
(add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
(easy-menu-add proof-response-mode-menu proof-response-mode-map)
@@ -84,7 +84,7 @@
;;;###autoload
(defun proof-response-config-done ()
- "Complete initialisation of a response-mode derived buffer."
+ "Complete initialization of a response-mode derived buffer."
(setq font-lock-defaults '(proof-response-font-lock-keywords)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 07ff560fb..ca3da8a3e 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -177,7 +177,7 @@ If called interactively, NUM is given by the prefix argument."
Calls `proof-assert-until-point' or `proof-retract-until-point' as
appropriate.
With prefix argument RAW, the activation of the omit proofs feature
-(`proof-omit-proofs-option') is temporarily toggled,
+\(`proof-omit-proofs-option') is temporarily toggled,
so we can chose whether to check all proofs in the asserted region,
or to merely assume them and save time."
(interactive "P")
@@ -215,7 +215,7 @@ If inside a comment, just process until the start of the comment."
(defun proof-process-buffer (&optional raw)
"Process the current (or script) buffer, and maybe move point to the end.
With prefix argument RAW, the activation of the omit proofs feature
-(`proof-omit-proofs-option') is temporarily toggled,
+\(`proof-omit-proofs-option') is temporarily toggled,
so we can chose whether to check all proofs in the asserted region,
or to merely assume them and save time."
(interactive "P")
@@ -593,7 +593,7 @@ last use time, to discourage saving these into the users database."
'(proof-add-completions))
(defun proof-script-complete (&optional arg)
- "Like `complete' but case-fold-search set to `proof-case-fold-search'."
+ "Like `complete' but `case-fold-search' set to `proof-case-fold-search'."
(interactive "*p")
;; completion not autoloaded in GNU Emacs
;; FIXME: It's probably because we shouldn't use it ;-)
@@ -613,13 +613,13 @@ last use time, to discourage saving these into the users database."
(defun proof-check-annotate-source (proof-results annotate-passing)
"Annotate proofs in current buffer according to PROOF-RESULTS.
PROOF-RESULTS must be the return value of `proof-check-proofs' or
-`proof-check-chunks' for the current buffer. This function
+`proof-check-chunks' for the current buffer. This function
annotates failing proofs with a comment containing \"FAIL\" and,
-if annotate-passing is non-nil, also passing proofs with
-\"PASS\". The annotation will be right aligned in the line
-according to `proof-check-annotate-position'. The position for
+if ANNOTATE-PASSING is non-nil, also passing proofs with
+\"PASS\". The annotation will be right aligned in the line
+according to `proof-check-annotate-position'. The position for
right alignment is configured in
-`proof-check-annotate-right-margin'. Existing \"PASS\" or
+`proof-check-annotate-right-margin'. Existing \"PASS\" or
\"FAIL\" annotations are deleted together with the surrounding
white space."
(let ((goal-column (or proof-check-annotate-right-margin fill-column)))
@@ -658,7 +658,7 @@ white space."
"Report `proof-check-proofs' results in PROOF-RESULTS in special buffer.
Report the results of `proof-check-proofs' in buffer
`proof-check-report-buffer' in human readable form or, if TAP is
-not nil, in test anything protocol (TAP). If BATCH is not nil,
+not nil, in test anything protocol (TAP). If BATCH is not nil,
report the results via message, such that they appear on stdout
when Emacs runs in batch mode or, when BATCH is a string, write
the results to the file denoted by BATCH."
@@ -723,27 +723,27 @@ the results to the file denoted by BATCH."
(defun proof-check-chunks (chunks)
"Worker function for `proof-check-proofs' for processing CHUNKS.
CHUNKS must be the reversed result of `proof-script-omit-filter'
-for a whole buffer. (Only the top-level must be reversed, the
+for a whole buffer. (Only the top-level must be reversed, the
commands inside the chunks must be as returned by
`proof-script-omit-filter', that is in reversed order.) CHUNKS
must not contain any 'nested-proof chunk.
This function processes the content of CHUNKS normally by
-asserting them one by one. Any error reported inside a 'no-proof
-chunk is reported as error to the user. 'proof chunks containing
+asserting them one by one. Any error reported inside a 'no-proof
+chunk is reported as error to the user. 'proof chunks containing
errors are silently replaced by
-`proof-script-proof-admit-command'. The result is a list of proof
-status results, one for each 'proof chunk in the same order. Each
+`proof-script-proof-admit-command'. The result is a list of proof
+status results, one for each 'proof chunk in the same order. Each
proof-status result is a list of 4 elements as follows.
-- 1st: proof status as `t' or `nil'. Proofs closed with a match
+- 1st: proof status as t or nil. Proofs closed with a match
of `proof-omit-cheating-regexp', if defined, count as failing,
- i.e., their status is `nil'.
+ i.e., their status is nil.
- 2nd: the name of the proof as reported by
`proof-get-proof-info-fn'.
- 3rd: Position of the start of the span containing the theorem
- to prove. More precisely, it is the second last span of the
- 'no-proof chunk before the 'proof chunk. Note that spans
- usually contain preceeding white space. Therefore this position
+ to prove. More precisely, it is the second last span of the
+ 'no-proof chunk before the 'proof chunk. Note that spans
+ usually contain preceding white space. Therefore this position
is not necessarily the first letter of the keyword introducing
the theorem statement.
- 4rd: Position of the start of the span containing \"Proof
@@ -834,7 +834,7 @@ proof-status result is a list of 4 elements as follows.
(defun proof-check-proofs ()
"Check proofs in current buffer and return a list of proof status results.
This is the internal worker for `proof-check-report' and
-`proof-check-annotate'.
+`proof-check-annotate'.
Reset scripting and then check all opaque proof in the current
buffer, relying on the omit-proofs feature, see
@@ -873,7 +873,7 @@ This function does not (re-)compile required files."
"Generate an overview about valid and invalid proofs.
This command completely processes the current buffer and
generates an overview about all the opaque proofs in it and
-whether their proof scripts are valid or invalid. Note that
+whether their proof scripts are valid or invalid. Note that
proofs closed with a cheating command (see
`proof-omit-cheating-regexp'), i.e., Admitted for Coq, count as
invalid.
@@ -885,20 +885,20 @@ the most interesting or challenging point instead of on the first
invalid proof.
Argument TAP, which can be set by a prefix argument, controls the
-form of the generated overview. Nil, without prefix, gives an
+form of the generated overview. Nil, without prefix, gives an
human readable overview, otherwise it's test anything
-protocol (TAP). Argument BATCH controls where the overview goes
-to. If nil, or in an interactive call, the overview appears in
-`proof-check-report-buffer'. If BATCH is a string, it should be a
-filename to write the overview to. Otherwise the overview is
+protocol (TAP). Argument BATCH controls where the overview goes
+to. If nil, or in an interactive call, the overview appears in
+`proof-check-report-buffer'. If BATCH is a string, it should be a
+filename to write the overview to. Otherwise the overview is
output via `message' such that it appears on stdout when this
command runs in batch mode.
In the same way as the omit-proofs feature, this command only
-tolerates errors inside scripts of opaque proofs. Any other error
-is reported to the user without generating an overview. The
+tolerates errors inside scripts of opaque proofs. Any other error
+is reported to the user without generating an overview. The
overview only contains those names of theorems whose proof
-scripts are classified as opaque by the omit-proofs feature. For
+scripts are classified as opaque by the omit-proofs feature. For
Coq for instance, among others, proof scripts terminated with
'Defined' are not opaque and do not appear in the generated
overview.
@@ -911,15 +911,15 @@ instance by asserting all require commands beforehand."
(defun proof-check-annotate (annotate-passing &optional save-buffer)
"Annotate failing proofs in current buffer with a \"FAIL\" comment.
-This function modifies the current buffer in place. Use with
+This function modifies the current buffer in place. Use with
care!
Similarly to `proof-check-report', check all opaque proofs in the
-current buffer. Instead of generating a report, failing proofs
-are annotated with \"FAIL\" in a comment. Existing \"PASS\" or
+current buffer. Instead of generating a report, failing proofs
+are annotated with \"FAIL\" in a comment. Existing \"PASS\" or
\"FAIL\" comments (e.g., from a previous run) are deleted
-together with the surrounding white space. With prefix argument
-(or when ANNOTATE-PASSING is non-nil) also passing proofs are
+together with the surrounding white space. With prefix argument
+\(or when ANNOTATE-PASSING is non-nil) also passing proofs are
annotated with a \"PASS\" comment. Pass and fail comments can be
placed at the last or second last statement before the opaque
proof. For Coq this corresponds to the proof using and the
@@ -1266,7 +1266,7 @@ If called interactively, STRING defaults to the current word near point."
(if string (pg-identifier-query string)))
(defun pg-identifier-query (identifier &optional ctxt callback)
- "Query the proof assisstant about the given IDENTIFIER.
+ "Query the proof assistant about the given IDENTIFIER.
This uses `proof-query-identifier-command'.
Parameter CTXT allows to give a context for the identifier (which
allows for multiple name spaces).
@@ -1584,7 +1584,7 @@ If ARG is omitted, nil, or not numeric, it takes the value 1.
It performs each of the desired undos checking that these operations will
not affect the locked region, obeying `proof-strict-read-only' if required.
-If strict read only behaviour is enforced, the user is queried whether to
+If strict read only behavior is enforced, the user is queried whether to
retract before the undo is allowed. If automatic retraction is enabled,
the retract and undo will go ahead without querying the user.
@@ -1613,7 +1613,7 @@ the locked region."
"This function is intended to be called by `pg-protected-undo'.
The flag ARG is passed to functions `undo' and `next-undo-elt'.
-It should be a non-numeric value saying whether an undo-in-region
+It should be a non-numeric value saying whether an `undo-in-region'
behavior is expected."
;; Note that if ARG is non-nil, (> (region-end) (region-beginning)) must hold,
;; at least for the first call from the loop of `pg-protected-undo'.
@@ -1642,7 +1642,7 @@ behavior is expected."
(defun next-undo-elt (arg)
"Return the undo element that will be processed on next undo/redo.
-Assume the undo-in-region behavior will apply if ARG is non-nil."
+Assume the `undo-in-region' behavior will apply if ARG is non-nil."
(let ((undo-list (if arg ; handle "undo in region"
(undo-make-selective-list
(region-beginning) (region-end)) ; can be '(nil)
@@ -1678,7 +1678,7 @@ Assume the undo-in-region behavior will apply if ARG is non-nil."
;;;###autoload
(defun proof-autosend-enable (&optional nomsg)
- "Enable or disable autosend behaviour."
+ "Enable or disable autosend behavior."
(if proof-autosend-timer
(cancel-timer proof-autosend-timer))
(when proof-autosend-enable
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index be696b2ef..7cc43f448 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -48,7 +48,7 @@ stub defined in proof-site, from names given in `proof-assistant-table'.")
Used for automatic configuration based on standard variable names.
Settings will be found by looking for names beginning with this
symbol as a prefix.
-Non-nil indicates PG has been initialised for an assistant.
+Non-nil indicates PG has been initialized for an assistant.
If this is nil, the hook functions in `proof-ready-for-assistant-hook'
are yet to be run.
@@ -78,7 +78,7 @@ stub defined in proof-site to -mode.")
(defvar proof-ready-for-assistant-hook nil
"Hook functions to run after PG is configured for a proof assistant.
-These functions allow late initialisation, once the choice of prover
+These functions allow late initialization, once the choice of prover
has been set.")
diff --git a/generic/pg-xml.el b/generic/pg-xml.el
index ca2bfd874..501727ce9 100644
--- a/generic/pg-xml.el
+++ b/generic/pg-xml.el
@@ -59,7 +59,7 @@
(defun pg-xml-parse-buffer (&optional buffer nomsg start end)
- "Parse an XML documment in BUFFER (defaulting to current buffer).
+ "Parse an XML document in BUFFER (defaulting to current buffer).
Display progress message unless NOMSG is non-nil.
Parsing according to `xml-parse-file' of xml.el.
Optional START and END bound the parse."
diff --git a/generic/proof-auxmodes.el b/generic/proof-auxmodes.el
index a77491261..dfeb42654 100644
--- a/generic/proof-auxmodes.el
+++ b/generic/proof-auxmodes.el
@@ -41,7 +41,7 @@ The test loads optional prover-specific config in -maths-menu.el"
;; Unicode tokens
;;
(defun proof-unicode-tokens-support-available ()
- "A test to see whether unicode tokens support is available."
+ "A test to see whether Unicode tokens support is available."
;; Requires prover-specific config in -unicode-tokens.el
;; Loaded before unicode-tokens.el to allow load-time config there
(proof-try-require (proof-ass-sym unicode-tokens)))
diff --git a/generic/proof-config.el b/generic/proof-config.el
index ed0703c10..591acf769 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -130,7 +130,7 @@ Used for Proof General's help menu."
(defcustom proof-info-command nil
"Command to ask for help or information in the proof assistant.
-String or fn. If a string, the command to use.
+String or function. If a string, the command to use.
If a function, it should return the command string to insert."
:type '(choice string function)
:group 'prover-config)
@@ -141,7 +141,7 @@ If a function, it should return the command string to insert."
:group 'prover-config)
(defcustom proof-goal-command nil
- "Command to set a goal in the proof assistant. String or fn.
+ "Command to set a goal in the proof assistant. String or function.
If a string, the format character `%s' will be replaced by the
goal string.
If a function, it should return the command string to insert."
@@ -149,7 +149,7 @@ If a function, it should return the command string to insert."
:group 'prover-config)
(defcustom proof-save-command nil
- "Command to save a proved theorem in the proof assistant. String or fn.
+ "Command to save a proved theorem in the proof assistant. String or function.
If a string, the format character `%s' will be replaced by the
theorem name.
If a function, it should return the command string to insert."
@@ -157,7 +157,7 @@ If a function, it should return the command string to insert."
:group 'prover-config)
(defcustom proof-find-theorems-command nil
- "Command to search for a theorem containing a given term. String or fn.
+ "Command to search for a theorem containing a given term. String or function.
If a string, the format character `%s' will be replaced by the term.
If a function, it should return the command string to send."
:type '(choice string function)
@@ -400,7 +400,7 @@ NB: This setting is not used for matching output from the prover."
:group 'proof-script)
(defcustom proof-show-proof-diffs-regexp nil
- "Matches all \"Show Proof\" forms (specific to the Coq prover)."
+ "Matches all \"Show Proof\" forms (specific to the Coq prover)."
:type 'regexp
:group 'proof-script)
@@ -697,9 +697,9 @@ needed for Coq."
:group 'proof-script)
(defcustom proof-omit-proofs-configured nil
- "t if the omit proofs feature has been configured by the proof assitant.
+ "Non-nil if the omit proofs feature has been configured by the proof assistant.
See also `proof-omit-proofs-option' or the Proof General manual
-for a description of the feature. This option can only be set, if
+for a description of the feature. This option can only be set, if
all of `proof-script-proof-start-regexp',
`proof-script-proof-end-regexp',
`proof-script-definition-end-regexp' and
@@ -713,7 +713,7 @@ commands in the source following a match of
`proof-script-proof-start-regexp' up to and including the next
match of `proof-script-proof-end-regexp', are omitted (not send
to the proof assistant) and replaced by
-`proof-script-proof-admit-command'. If a match for
+`proof-script-proof-admit-command'. If a match for
`proof-script-definition-end-regexp' is found while searching
forward for the proof end or if
`proof-script-cmd-prevents-proof-omission' recognizes a proof
@@ -724,7 +724,7 @@ to and including the match of
and not omitted, thus all these proof commands _are_ sent to the
proof assistant.
-The feature does not work for nested proofs. If a match for
+The feature does not work for nested proofs. If a match for
`proof-script-proof-start-regexp' is found before the next match
for `proof-script-proof-end-regexp' or
`proof-script-definition-end-regexp', the search for opaque
@@ -741,11 +741,11 @@ without surrounding space."
(defcustom proof-omit-cheating-regexp nil
"Regular expression matching proof closing commands for incomplete proofs.
If set, this regular expression is applied to the last command of
-opaque proofs. If it matches the proofs counts as invalid for the
-proof-status statistics and annotation feature. For Coq this is
+opaque proofs. If it matches the proofs counts as invalid for the
+proof-status statistics and annotation feature. For Coq this is
used to mark Admitted proofs as invalid.
-This option can be left at `nil'."
+This option can be left at nil."
:type 'regexp
:group 'proof-script)
@@ -777,11 +777,11 @@ See `proof-omit-proofs-configured'."
(defcustom proof-script-cmd-prevents-proof-omission nil
"Optional predicate to match commands that prevent omitting the current proof.
If set, this option should contain a function that takes a proof
-command (as string) as argument and returns t or nil. If set, the
+command (as string) as argument and returns t or nil. If set, the
function is called on every proof command inside a proof while
-scanning for proofs to omit. The predicate should return t if the
-command has effects ouside the proof, potentially breaking the
-script if the current proof is omitted. If the predicate returns
+scanning for proofs to omit. The predicate should return t if the
+command has effects outside the proof, potentially breaking the
+script if the current proof is omitted. If the predicate returns
t, the proof is considered to be not opaque and thus not omitted."
:type 'function
:group 'proof-script)
@@ -790,9 +790,9 @@ t, the proof is considered to be not opaque and thus not omitted."
"Optional regexp for commands that prevent omitting the next proof.
If set, this option should contain a regular expression that
matches proof-script commands that prevent the omission of proofs
-dirctly following this command. When scanning the newly asserted
+directly following this command. When scanning the newly asserted
region for proofs to omit, every proof-script command outside
-proofs is matched against this regexp. If it matches and the next
+proofs is matched against this regexp. If it matches and the next
command matches `proof-script-proof-start-regexp' this following
proof will not be omitted.
@@ -811,10 +811,10 @@ asserted together."
(defcustom proof-get-proof-info-fn nil
"Return proof name and state number for `proof-check-proofs'.
-Proof assistant specific function for `proof-check-proofs'. This
+Proof assistant specific function for `proof-check-proofs'. This
function takes no arguments, it is called after completely
processing the proof script up to a certain point (including all
-callbacks in spans). It must return a list, which contains, in
+callbacks in spans). It must return a list, which contains, in
the following order:
* the current state number (as positive integer)
@@ -826,7 +826,7 @@ Processing the command returned by `proof-retract-command-fn'
without processing any other command after calling this function
should be a no-op.
-(This function has the same signature and specification as
+\(This function has the same signature and specification as
`proof-tree-get-proof-info'.)"
:type 'function
:group 'proof-script)
@@ -834,7 +834,7 @@ should be a no-op.
(defcustom proof-retract-command-fn nil
"Function for retract command to a certain state.
This function takes a state as argument as returned by
-`proof-get-proof-info-fn'. It should return a command that brings
+`proof-get-proof-info-fn'. It should return a command that brings
the proof assistant back to the same state."
:type 'function
:group 'proof-script)
@@ -995,7 +995,7 @@ If `proof-terminal-string' is nil, this has no effect."
"The command for configuring the proof process to gain synchronization.
This command is sent before Proof General's synchronization
mechanism is engaged, to allow customization inside the process
-to help gain syncrhonization (e.g. engaging special markup).
+to help gain synchronization (e.g. engaging special markup).
It is better to configure the proof assistant for this purpose
via command line options if possible, in which case this variable
@@ -1023,7 +1023,7 @@ See also `proof-shell-pre-sync-init-cmd'."
:group 'proof-shell)
(defcustom proof-shell-restart-cmd ""
- "A command for re-initialising the proof process."
+ "A command for re-initializing the proof process."
:type '(choice string (const nil))
:group 'proof-shell)
@@ -1198,7 +1198,7 @@ It is safe to leave this variable unset (as nil)."
"Regexp matching a non-error from the proof assistant.
Some commands of the proof assistant may display error message as
-information messages. E.g. in Coq: \"Fail \" shows the error
+information messages. E.g. in Coq: \"Fail \" shows the error
message thrown by without failing itself.
Matching this regexp disables error message detection.
@@ -1322,7 +1322,7 @@ is shown to the user. Set to nil to disable."
"Regexp matching the start of the proof state output.
This is an important setting. Output between `proof-shell-start-goals-regexp'
and `proof-shell-end-goals-regexp' will be pasted into the goals buffer
-and possibly analysed further for proof-by-pointing markup.
+and possibly analyzed further for proof-by-pointing markup.
If it is left as nil, the goals buffer will not be used.
The goals display starts at the beginning of the match on this
@@ -1371,7 +1371,7 @@ parsing later. Note that this affects processing of output which is
ordinarily accumulated: output which appears before the eager annotation
start will be discarded.
-The start/end annotations can be used to hilight the output, but
+The start/end annotations can be used to highlight the output, but
are stripped from display of the message in the minibuffer.
It is useful to recognize (starts of) warnings or file-reading messages
@@ -1618,8 +1618,7 @@ This function takes no argument and should use
`proof-shell-last-prompt' and `proof-shell-last-output' to
determine whether the last command ended up inside a
proof (either by remaining inside one or opening a new one), or
-outside of any proof.
-"
+outside of any proof."
:type 'function
:group 'proof-script)
@@ -1662,7 +1661,7 @@ tokens (for example, editing documentation or source code files)."
"Whether communication between PG and prover is 8bit clean.
If non-nil, no special non-ASCII characters must be used in markup.
If so, the process coding system will be set to UTF-8.
-With old systems that may use unsafe unicode prefix sequences
+With old systems that may use unsafe Unicode prefix sequences
\(i.e., lead to hanging in C-libraries), this should be set to nil."
:type 'boolean
:group 'proof-shell)
@@ -1742,7 +1741,7 @@ are normally the ones of interest:
'proof-done-advancing A \"forward\" scripting command
'proof-done-retracting A \"backward\" scripting command
'proof-done-invisible A non-scripting command
- 'proof-shell-set-silent Indicates prover output has been surpressed
+ 'proof-shell-set-silent Indicates prover output has been suppressed
'proof-shell-clear-silent Indicates prover output has been restored
'init-cmd Early initialization command sent to prover
@@ -1832,7 +1831,7 @@ tries to interrupt the proof process. It is therefore run earlier
than `proof-shell-handle-error-or-interrupt-hook', which runs
when the interrupt is acknowledged inside `proof-shell-exec-loop'.
-This hook also runs when the proof assistent is killed.
+This hook also runs when the proof assistant is killed.
Hook functions should set the dynamic variable `prover-was-busy'
to t if there might have been a reason to interrupt. Otherwise
@@ -1851,7 +1850,7 @@ before returning to the top level."
(defcustom proof-shell-handle-output-system-specific nil
"Set this variable to handle system specific output.
-Errors and interrupts are recognised in the function
+Errors and interrupts are recognized in the function
`proof-shell-handle-immediate-output'. Later output is
handled by `proof-shell-handle-delayed-output', which
displays messages to the user in *goals* and *response*
@@ -1880,7 +1879,7 @@ retracted, or after a command has been sent to the prover with
`proof-shell-invisible-command'.
It is run *before* the generic processing of the command span is
-done (see function `prof-done-advancing'). See
+done (see function `prof-done-advancing'). See
`proof-state-change-hook' to insert actions after it."
:type '(repeat function)
:group 'proof-shell)
@@ -1892,7 +1891,7 @@ retracted, or after a command has been sent to the prover with
`proof-shell-invisible-command'.
It is run *after* the generic processing of the command span is
-done (see function `prof-done-advancing'). See
+done (see function `prof-done-advancing'). See
`proof-state-change-pre-hook' to insert actions before it.
This hook may be used to refresh the toolbar."
@@ -1912,7 +1911,7 @@ the theorem being saved."
(defcustom proof-dependency-menu-system-specific nil
"Hook for system specific menu items for dependency menu.
This must be a function taking one argument: the span one which
-the secific menu must be added. It must return a lit with the
+the specific menu must be added. It must return a lit with the
same type as `proof-dependency-in-span-context-menu' returns."
:type '(repeat function)
:group 'proof-shell)
@@ -1952,7 +1951,7 @@ Leave unset if no special characters are being used."
;; FIXME: The docstring suggest we should use t!?
"Choice of syntax tree encoding for terms.
-If nil, prover is expected to make no optimisations.
+If nil, prover is expected to make no optimizations.
If non-nil, the pretty printer of the prover only reports local changes.
For Coq 6.2, use t."
:type 'boolean
@@ -2052,7 +2051,7 @@ See also `proof-script-font-lock-keywords' and `proof-goals-font-lock-keywords'.
:group 'proof-goals)
(defcustom proof-shell-font-lock-keywords nil
- "Value of `font-lock-keywords' used to fontify the shell buiffer.
+ "Value of `font-lock-keywords' used to fontify the shell buffer.
The shell mode should may this before calling `proof-response-config-done'.
Note that by default, font lock is turned *off* in shell buffers to
improve performance. If you need to understand some output it may help
@@ -2071,7 +2070,7 @@ the current restriction, and must return the final value of (point-max).
:group 'proof-goals)
(defcustom pg-after-fontify-output-hook nil
- "This hook is called before fonfitying a region in an output buffer.
+ "This hook is called before fontifying a region in an output buffer.
\[This hook is presently only used by Isabelle]."
:type '(repeat function)
:group 'proof-goals)
diff --git a/generic/proof-depends.el b/generic/proof-depends.el
index dd224424b..1917ecc0a 100644
--- a/generic/proof-depends.el
+++ b/generic/proof-depends.el
@@ -47,7 +47,7 @@ i.e.: ((file-name-1 (def1 def2 def3)) (file-name-2 (def1 def2 def3)))")
(defun proof-depends-module-name-for-buffer ()
"Return a module name for the current buffer.
This is a name that the prover prefixes all item names with.
-For example, in isabelle, a file Stuff.ML contains theorems with
+For example, in Isabelle, a file Stuff.ML contains theorems with
fully qualified names of the form Stuff.theorem1, etc.
For other provers, this function may need modifying."
(if buffer-file-name
@@ -221,7 +221,7 @@ NAMEFN is applied to each element of LIST to make the names."
(vector name nil nil)))
(defun proof-make-highlight-depts-menu (name fn span prop)
- "Return a menu item that for highlighting dependents/depencies of SPAN."
+ "Return a menu item that for highlighting dependents/dependencies of SPAN."
(let ((deps (span-property span prop)))
(vector name `(,fn ,(span-property span 'name) (quote ,deps))
(not (not deps)))))
diff --git a/generic/proof-faces.el b/generic/proof-faces.el
index 322fdd14c..7473fc268 100644
--- a/generic/proof-faces.el
+++ b/generic/proof-faces.el
@@ -54,7 +54,7 @@ If you are on a window system and your value of variable `window-system' is
not listed here, you may not get the correct syntax colouring behaviour.")
(defmacro proof-face-specs (bl bd ow)
- "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
+ "Return a spec for `defface' with BL for light background, BD for dark, OW o/w."
`(append
(apply 'append
(mapcar
@@ -207,7 +207,7 @@ Warning messages can come from proof assistant or from Proof General itself."
(:background "indianred1")
(:background "indianred3")
(:underline t))
- "Proof General face for marking an error in the proof script. "
+ "Proof General face for marking an error in the proof script."
:group 'proof-faces)
(defface proof-script-highlight-error-face
@@ -215,7 +215,7 @@ Warning messages can come from proof assistant or from Proof General itself."
(:background "indianred1" :bold t)
(:background "indianred3" :bold t)
(:underline t :bold t))
- "Proof General face for highlighting an error in the proof script. "
+ "Proof General face for highlighting an error in the proof script."
:group 'proof-faces)
(defface proof-omitted-proof-face
@@ -223,7 +223,7 @@ Warning messages can come from proof assistant or from Proof General itself."
(:background "#EAEFFF" :extend t)
(:background "#9C4A90" :extend t)
(:foreground "white" :background "black" :extend t))
- "*Face for background of omitted proofs"
+ "*Face for background of omitted proofs."
:group 'proof-faces)
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index db2a3b9d5..f9801bbae 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -167,7 +167,7 @@ without adjusting window layout."
(easy-menu-define
proof-mode-menu
(list proof-mode-map proof-splash-mode-map)
- "The main Proof General menu"
+ "The main Proof General menu."
(proof-main-menu)))
;; The proof assistant specific menu
@@ -644,7 +644,7 @@ without adjusting window layout."
;;
(defun proof-set-document-centred ()
- "Select options for document-centred working."
+ "Select options for document-centered working."
(interactive)
(proof-full-annotation-toggle 1)
(proof-auto-raise-toggle 0)
@@ -867,7 +867,7 @@ suitable for adding to the proof assistant menu."
(defun proof-add-favourite (command inscript menuname &optional key)
- "Define and add a \"favourite\" proof-assisant function to the menu bar.
+ "Define and add a \"favourite\" proof-assistant function to the menu bar.
The favourite function will issue COMMAND to the proof assistant.
COMMAND is inserted into script (not sent immediately) if INSCRIPT non-nil.
MENUNAME is the name of the function for the menu.
diff --git a/generic/proof-script.el b/generic/proof-script.el
index d62f2ea54..133a4f132 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -283,7 +283,7 @@ Otherwise set the locked region to be from (point-min) to END."
;; ** Initialise spans for a buffer
(defun proof-init-segmentation ()
- "Initialise the queue and locked spans in a proof script buffer.
+ "Initialize the queue and locked spans in a proof script buffer.
Allocate spans if need be. The spans are detached from the
buffer, so the regions are made empty by this function.
Also clear list of script portions."
@@ -715,7 +715,7 @@ This is based on its name and type.
Each span has a 'type property, one of:
'goalsave A goal..savegoal region in the buffer, a completed proof.
- 'vanilla Initialised in proof-semis-to-vanillas, for
+ 'vanilla Initialized in proof-semis-to-vanillas, for
'comment A comment outside a command.
'proverproc A region closed by the prover, processed outwith PG
'pbp A PBP command inserted automatically into the script."
@@ -1045,7 +1045,7 @@ scripting buffer, according to ACTION.
Retract buffer BUFFER if set, otherwise use the current buffer.
Gives a message in the minibuffer and busy-waits for the retraction
or processing to complete. If it fails for some reason,
-an error is signalled here."
+an error is signaled here."
(unless (or (eq action 'process) (eq action 'retract))
(error "Invalid argument (in proof-protected-process-or-retract)"))
(let ((buf (or buffer (current-buffer))))
@@ -1376,7 +1376,7 @@ With ARG, turn on scripting iff ARG is positive."
"The callback function for `assert-until-point'.
Argument SPAN has just been processed.
-This is the callback for all the normal commands. Besides stuff
+This is the callback for all the normal commands. Besides stuff
that is not yet documented here, this function
- extends the locked region
- creates additional spans (without 'type property) for help,
@@ -1997,9 +1997,9 @@ Assumes that point is at the end of a command."
(defun proof-move-over-whitespace-to-next-line (pos)
"Return position of next line if one needs only to jump over white space.
-Utility function. In the current buffer, check if beginning of
+Utility function. In the current buffer, check if beginning of
next line can be reached from POS by moving over white
-space (spaces, tabs) only. If yes return the beginning of next
+space (spaces, tabs) only. If yes return the beginning of next
line, otherwise POS."
(save-excursion
(goto-char pos)
@@ -2017,36 +2017,36 @@ and those which can not be omitted (either outside proofs or
inside proofs that cannot be omitted).
See `proof-omit-proofs-configured' for the description of the
-omit proofs feature. This function uses
+omit proofs feature. This function uses
`proof-script-proof-start-regexp',
`proof-script-proof-end-regexp' and
`proof-script-definition-end-regexp' to search for complete
-opaque proofs in the action list VANILLAS. Additionally, it uses
+opaque proofs in the action list VANILLAS. Additionally, it uses
`proof-script-cmd-prevents-proof-omission' and
`proof-script-cmd-force-next-proof-kept' to detect proofs that
cannot be omitted.
The result is a list of chunks, where each chunk is a list that
-contains a type tag as first element. The chunk list is returned
+contains a type tag as first element. The chunk list is returned
in reversed order, i.e., the first vanilla span in VANILLAS is
inside the last chunk.
There are three types of chunks: 'proof for commands inside a
proof that can be omitted, 'no-proof for commands that are
outside a proof or cannot be omitted, and 'nested for commands
-that contain a nested proof. Note that there may be several
+that contain a nested proof. Note that there may be several
adjacent 'no-proof chunks, for instance for commands outside a
proof followed by a proof that cannot be omitted.
The 'proof chunk has 4 elements:
-('proof proof-cmds-reversed span-start-first-proof-cmd span-end-first-proof-cmd)
+\('proof proof-cmds-reversed span-start-first-proof-cmd span-end-first-proof-cmd)
The second, proof-cmds-reversed, contains the vanilla spans from
VANILLAS corresponding to commands belonging to a proof,
excluding the first that matched
`proof-script-proof-start-regexp' and including the last that
-matched `proof-script-proof-end-regexp' in reversed order. The
+matched `proof-script-proof-end-regexp' in reversed order. The
third element span-start-first-proof-cmd is the position of the
start of the command that matched
`proof-script-proof-start-regexp' and span-end-first-proof-cmd is
@@ -2054,18 +2054,18 @@ the position of the end of that command.
The 'no-proof chunk has 2 elements.
-('no-proof cmds-reversed)
+\('no-proof cmds-reversed)
cmds-reversed contains the vanilla spans of VANILLAS in reversed
order.
The 'nested-proof chunk has 3 elements.
-('nested-proof cmds-reversed line-number-nested-proof)
+\('nested-proof cmds-reversed line-number-nested-proof)
line-number-nested-proof is the line number where the nested
-proof was detected. cmds-reversed is the tail of VANILLAS,
-containing the start of the nested proof, in reversed order. If
+proof was detected. cmds-reversed is the tail of VANILLAS,
+containing the start of the nested proof, in reversed order. If
there is a 'nested-proof chunk in the result, it is the first
chunk."
(cl-assert
@@ -2190,17 +2190,17 @@ chunk."
(defun proof-script-omit-proofs (vanillas)
"Return a copy of VANILLAS with complete opaque proofs omitted.
See `proof-omit-proofs-configured' for the description of the
-omit proofs feature. This function uses
+omit proofs feature. This function uses
`proof-script-proof-start-regexp',
`proof-script-proof-end-regexp' and
`proof-script-definition-end-regexp' to search for complete
-opaque proofs in the action list VANILLAS. Additionally, it uses
+opaque proofs in the action list VANILLAS. Additionally, it uses
`proof-script-cmd-prevents-proof-omission' and
`proof-script-cmd-force-next-proof-kept' to detect proofs that
-cannot be omitted. Complete opaque proofs are replaced by
-`proof-script-proof-admit-command'. The span of the admit command
+cannot be omitted. Complete opaque proofs are replaced by
+`proof-script-proof-admit-command'. The span of the admit command
contains an 'omitted-proof-region property with the region of the
-omitted proof. This is used in `proof-done-advancing-save' to
+omitted proof. This is used in `proof-done-advancing-save' to
colour the omitted proof with `proof-omitted-proof-face'.
Display a warning if another proof start is found inside a
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 690b2c3da..4df977868 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -21,14 +21,14 @@
;;
;; A big portion of the code in this file implements the callback
;; function that Emacs calls when output arrives from the proof
-;; assistant. This callback implements a major feature of Proof
+;; assistant. This callback implements a major feature of Proof
;; General: Sending one command after the other to the proof assistant
;; and processing/displaying the reply.
;;
;; The following documents the call graph of important functions that
-;; contribute to this callback. The entry point is
+;; contribute to this callback. The entry point is
;; `proof-shell-filter-wrapper', which is configured in
-;; `scomint-output-filter-functions'. Sending the next comand to the
+;; `scomint-output-filter-functions'. Sending the next command to the
;; proof assistant and calling the callbacks of the spans happens in
;; `proof-shell-exec-loop'.
;;
@@ -135,7 +135,7 @@ bother the user. They may include
show command when running silent.
Note that 'invisible does not imply any of the others. If flags
-are non-empty, interactive cues will be surpressed. (E.g.,
+are non-empty, interactive cues will be suppressed. (E.g.,
printing hints).
See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
@@ -145,11 +145,11 @@ See the functions `proof-start-queue' and `proof-shell-exec-loop'.")
When the proof assistant is busy, one cannot push to the head of
`proof-action-list`, because the head usually (but not always)
contains the item that the proof assistant is currently
-executing. This list therefore holds the items to be executed
-before any other items in `proof-action-list'. Inside
+executing. This list therefore holds the items to be executed
+before any other items in `proof-action-list'. Inside
`proof-shell-exec-loop', when `proof-action-list' is in the right
state, the content of this list is prepended to
-`proof-action-list'. Use `proof-add-to-priority-queue' to add
+`proof-action-list'. Use `proof-add-to-priority-queue' to add
items to this priority list, to ensure the proof assistant starts
running, in case `proof-action-list' is currently empty.
@@ -196,19 +196,19 @@ background compilation finishes. Then those items are put into
"Position of end of second last input inside delayed callbacks.
When callbacks of action items are processed, `proof-marker' has already
been advanced to the end of the next input that the proof assistant
-processes in parallel with the callback. This variable permits the
+processes in parallel with the callback. This variable permits the
callback to access the end of the input belonging to its action-list
item and then process the complete output that the proof assistant has
sent.")
(defvar proof-shell-delayed-output-start nil
"A record of the start of the previous output in the shell buffer.
-The previous output is held back for processing at end of queue. Reset
+The previous output is held back for processing at end of queue. Reset
in `proof-shell-filter', i.e., when subsequent output arrives.")
(defvar proof-shell-delayed-output-end nil
"A record of the start of the previous output in the shell buffer.
-The previous output is held back for processing at end of queue. Reset
+The previous output is held back for processing at end of queue. Reset
in `proof-shell-filter', i.e., when subsequent output arrives.")
(defvar proof-shell-delayed-output-flags nil
@@ -375,12 +375,11 @@ In this case `proof-shell-filter' must be called again after it finished.")
string)
(defvar proof-shell-before-process-hook nil
- "Functions run from `proof-shell-start' just before
- starting the prover process. Last chance to modify
- xxx-prog-args and xxx-prog-name")
+ "Functions run from `proof-shell-start' just before starting the prover process.
+Last chance to modify xxx-prog-args and xxx-prog-name")
(defun proof-shell-start ()
- "Initialise a shell-like buffer for a proof assistant.
+ "Initialize a shell-like buffer for a proof assistant.
Does nothing if proof assistant is already running.
Also generates goal and response buffers.
@@ -848,7 +847,7 @@ unless the FLAGS for the command are non-nil (see `proof-action-list')."
(defun proof-pbp-focus-on-first-goal ()
"If the `proof-goals-buffer' contains goals, bring the first one into view.
-This is a hook function for proof-shell-handle-delayed-output-hook."
+This is a hook function for `proof-shell-handle-delayed-output-hook'."
)
;; PG 4.0 FIXME
; (let
@@ -1169,8 +1168,8 @@ being processed."
"Start processing priority items if necessary.
If there are priority items and the proof shell is not busy with
other items, then this function starts the prover with the
-priority items. This function relies on the invariants of
-`proof-shell-filter-active' and on `proof-action-list'. The
+priority items. This function relies on the invariants of
+`proof-shell-filter-active' and on `proof-action-list'. The
latter is non-empty, if there is some item, which has not been
fully processed yet.
@@ -1188,7 +1187,7 @@ processed without calling this function."
(defun proof-add-to-priority-queue (queueitem)
"Add item to `proof-priority-action-list' and start the queue if necessary.
Argument QUEUEITEM must be an action item as documented for
-`proof-action-list'. Add flag 'priority-action to QUEUEITEM, such
+`proof-action-list'. Add flag 'priority-action to QUEUEITEM, such
that priority items can be recognized and the order of added
priority items can be preserved."
(let ((qi (list (car queueitem) (cadr queueitem) (cl-caddr queueitem)
@@ -1339,7 +1338,7 @@ contains only invisible elements for Prooftree synchronization."
(pg-processing-complete-hint))
(pg-finish-tracing-display))
- (and (not proof-second-action-list-active)
+ (and (not proof-second-action-list-active)
(let ((last-command (car (nth 1 (car (last proof-action-list))))))
(or (null proof-action-list)
(cl-every
@@ -1541,7 +1540,7 @@ entry point, `proof-shell-filter' against such parallel,
overlapping calls.
The argument STR-DO-NOT-USE contains the most recent output, but
-is discarded. `proof-shell-filter' collects the output from
+is discarded. `proof-shell-filter' collects the output from
`proof-shell-buffer' (where it is inserted by
`scomint-output-filter'), relieving this function from the task
to buffer the output that arrives during parallel, overlapping
@@ -1816,7 +1815,7 @@ will also be displayed in the response buffer.
For example, if OUTPUT has this form:
- MESSSAGE-1
+ MESSAGE-1
GOALS-1
MESSAGE-2
GOALS-2
@@ -2107,7 +2106,7 @@ Error messages are displayed as usual."
;;;###autoload
(define-derived-mode proof-shell-mode scomint-mode
- "proof-shell" "Proof General shell mode class for proof assistant processes"
+ "proof-shell" "Proof General shell mode class for proof assistant processes."
(setq proof-buffer-type 'shell)
diff --git a/generic/proof-splash.el b/generic/proof-splash.el
index e6ddadf82..4e7ca7612 100644
--- a/generic/proof-splash.el
+++ b/generic/proof-splash.el
@@ -92,7 +92,7 @@ Proof General."
)
"Evaluated to configure splash screen displayed when entering Proof General.
A list of the screen contents. If an element is a string or an image
-specifier, it is displayed centred on the window on its own line.
+specifier, it is displayed centered on the window on its own line.
If it is nil, a new line is inserted."
:type 'sexp
:group 'proof-general-internals)
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index e26ab1e6f..b19cf3162 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -45,15 +45,15 @@
;;
;; A fourth problem is that proof-tree display can only work when the
;; prover output is not suppressed (via `proof-full-annotation').
-;; `proof-shell-should-be-silent' takes care of that. For proof
+;; `proof-shell-should-be-silent' takes care of that. For proof
;; assistants that run completely silent,
;; `proof-tree-assistant-specific-urgent-action' should be configured
-;; to insert a show-goal command after each command. The callback of
+;; to insert a show-goal command after each command. The callback of
;; this proof action list item should be
;; `proof-tree-display-goal-callback'.
;;
;; Earlier versions of prooftree maintained certain data structures
-;; twice, one time in prooftree and one time in Proof General. The
+;; twice, one time in prooftree and one time in Proof General. The
;; copy in Proof General was necessary, because all necessary show
;; goal commands had to be generated and processed immediately in the
;; current state.
@@ -62,46 +62,46 @@
;; earlier state, therefore, in the current version all the processing
;; is done in prooftree and prooftree sends asynchronous show goal
;; requests to Proof General, if sequents are missing or must be
-;; updated. These show goal requests are processed in Proof General as
+;; updated. These show goal requests are processed in Proof General as
;; priority actions, nevertheless, they can be delayed for quite some
-;; time. It might even happen, that the first show goal command for an
+;; time. It might even happen, that the first show goal command for an
;; additionally spawned subgoal arrives at Proof General only after
-;; the proof has been finished. Prooftree can request additional
+;; the proof has been finished. Prooftree can request additional
;; sequent updates for instantiated existentials only after that first
-;; sequent has arrived. Prooftree keeps a tree with the instantiation
+;; sequent has arrived. Prooftree keeps a tree with the instantiation
;; dependencies of existentials, such that it can immediately issue
-;; all sequent update requests for all known instantiations. With this
+;; all sequent update requests for all known instantiations. With this
;; there is at most one round trip to prooftree necessary after a
;; proof has been finished in Proof General.
;;
;; In the proof assistant source code, the next lemma might start
-;; immediately after finishing the preceeding proof. Before processing
+;; immediately after finishing the preceding proof. Before processing
;; that next command, the proof tree display must be switched off in
;; Proof General and for Coq, the command for disabling the dependent
-;; evar line must be processed. On the other hand, all show goal
-;; commands arriving late for the preceeding proof must be completely
-;; processed with proof tree display enabled. To solve that problem,
+;; evar line must be processed. On the other hand, all show goal
+;; commands arriving late for the preceding proof must be completely
+;; processed with proof tree display enabled. To solve that problem,
;; `proof-tree-check-proof-finish' is called as urgent action via
;; `proof-tree-urgent-action' inside `proof-shell-exec-loop', before
;; the next command in the queue region is sent to the proof
-;; assistant. If this urgent action recognizes a proof end, it moves
+;; assistant. If this urgent action recognizes a proof end, it moves
;; all non-priority actions from `proof-action-list' to
;; `proof-tree--delayed-actions' signaling
-;; `proof-second-action-list-active'. This effectively stops
-;; processing of the queue region. When the end of the proof is
+;; `proof-second-action-list-active'. This effectively stops
+;; processing of the queue region. When the end of the proof is
;; processed in the delayed output handling, Proof General sends a
;; proof-complete message to prooftree, thereby requesting a
;; confirm-proof-complete from prooftree after prooftree has sent all
-;; show goal requests to Proof General. Via
+;; show goal requests to Proof General. Via
;; `proof-tree-display-stop-command' the confirmation message causes
;; the insertion of an action item with tag 'proof-tree-last-item.
;; When this item arrives inside `proof-tree-check-proof-finish', all
;; show goal commands have been processed, because care is taken to
-;; process priority actions in order. `proof-tree-check-proof-finish'
+;; process priority actions in order. `proof-tree-check-proof-finish'
;; can therefore move the queued commands back to `proof-action-list'
;; and continue normal processing.
;;
-;; Apart from the urgent action discussed before,
+;; Apart from the urgent action discussed before,
;; the glue code here works on the delayed output. That is,
;; the glue code here runs when the next proof command has already
;; been sent to the proof assistant. The glue code makes a light
@@ -118,7 +118,7 @@
;; Existential Variables command in Coq. There is one proof tree in
;; the first layer for the original goal. The second layer contains
;; all the goals that the first Grab Existential Variables command
-;; created from uninstantiated existential variabes in the main proof.
+;; created from uninstantiated existential variables in the main proof.
;; The third layer contains the goals that the second Grap Existential
;; Variables created.
@@ -134,7 +134,7 @@
;;
(defgroup proof-tree ()
- "Customization for the proof tree visualizer"
+ "Customization for the proof tree visualizer."
:group 'proof-general
:package-version '(ProofGeneral . "4.2"))
@@ -175,7 +175,7 @@ as Lemma, that can start a proof."
(defcustom proof-tree-navigation-command-regexp nil
"Regexp to match a navigation command.
-A navigation command typically focusses on a different open goal
+A navigation command typically focuses on a different open goal
without changing any of the open goals. Leave at nil if there are
no navigation commands."
:type '(choice regexp (const nil))
@@ -283,7 +283,7 @@ is retracted (but no stuff before X)."
"Proof assistant specific function for a show-goal command.
This function is applied to a goal ID and a state number and
should return a command (as string) that will display the
-complete sequent with that ID in the given state. The regexp
+complete sequent with that ID in the given state. The regexp
`proof-tree-update-goal-regexp' should match the output of the
proof assistant for the returned command, such that
`proof-tree-update-sequent' will update the sequent ID inside
@@ -317,9 +317,9 @@ must return a buffer position."
(defcustom proof-tree-start-display-hook ()
"Normal hook for prooftree when external display starts.
-This hook is called when the external display is startet, more
+This hook is called when the external display is started, more
precisely, when the proof assistant is in the state that Proof
-General starts to send display commands to prooftree. This means,
+General starts to send display commands to prooftree. This means,
retraction to the start of the proof, in case it was necessary,
has been done and `proof-action-list` is empty.
@@ -331,20 +331,20 @@ evars line."
(defcustom proof-tree-display-stop-command ()
"Function for the last command before switching off proof-tree display.
This is a proof assistant specific function that must be
-instantiated. When a proof finishes with proof-tree display,
+instantiated. When a proof finishes with proof-tree display,
prooftree may request a number of show goal commands after the
-proof has been finished in the proof assistant. This function
+proof has been finished in the proof assistant. This function
must return an action item that can be inserted as last command
in `proof-action-list' after all these show goal commands.
-For Coq this is used to disable the dependent evar line. But also
+For Coq this is used to disable the dependent evar line. But also
other proof assistants that enable the proof tree display must
set this function.
An action item is a list `(SPAN COMMANDS ACTION [DISPLAYFLAGS])',
-see `proof-action-list'. The action item must not be recognized
+see `proof-action-list'. The action item must not be recognized
as comment by `proof-shell-slurp-comments', that is COMMANDS must
-be a nonempty list of strings. The generic prooftree glue code
+be a nonempty list of strings. The generic prooftree glue code
will add 'proof-tree-last-item to DISPLAYFLAGS when necessary."
:type 'function
:group 'proof-tree-internals)
@@ -353,9 +353,9 @@ will add 'proof-tree-last-item to DISPLAYFLAGS when necessary."
"Function to perform proof assistant specific urgent actions.
If set, this function is called when the last proof-action item has just
been processed, before the next item is sent to the proof assistant and
-the callback of the last item is processed. It is guaranteed to be
+the callback of the last item is processed. It is guaranteed to be
called at a point at which `proof-action-list' can be directly
-manipulated. If no urgent action is needed, this option should be left
+manipulated. If no urgent action is needed, this option should be left
at nil."
:type 'function
:group 'proof-tree-internals)
@@ -412,15 +412,15 @@ This variable is only maintained and meaningful if
(defvar proof-tree--delayed-actions nil
"Hold delayed action items when waiting for prooftree after proof end.
This internal variable is completely managed by
-`proof-tree-check-proof-finish'. After a proof with proof-tree
+`proof-tree-check-proof-finish'. After a proof with proof-tree
display has been finished, it holds the following commands, until
-all requested show goal commands have been processed. If this
+all requested show goal commands have been processed. If this
variable is non-nil, then `proof-second-action-list-active' must
-be set. In addition to holding the to be delayed action items,
+be set. In addition to holding the to be delayed action items,
this variable is used to remember that
`proof-tree-check-proof-finish' waits for
`proof-tree-display-stop-command' after it recognized the end of
-a proof. Therefore, if non-nil, this variable must either hold a
+a proof. Therefore, if non-nil, this variable must either hold a
nonempty list (the to be delayed action items) or t (if there are
no action items to be delayed.")
@@ -431,8 +431,8 @@ no action items to be delayed.")
"Partition list L according to P.
Returns a cons pair `(L1 . L2)' of lists, where L1 contains the
elements of L for which P returns non-nil and L2 those for which
-P returns nil. The concatenation of L1 and L2 is a permutation of
-L, the order of elements in L is preserved. P must be a function
+P returns nil. The concatenation of L1 and L2 is a permutation of
+L, the order of elements in L is preserved. P must be a function
that takes one argument."
(let (yes no)
(dolist (x l (cons (nreverse yes) (nreverse no)))
@@ -450,8 +450,8 @@ This marker points to the next piece of output that needs to get processed.")
(defvar proof-tree-filter-continuation nil
"Continuation when `proof-tree-process-filter' stops early.
-A function that handles a command from Prooftee might fail
-because not all data from Prooftee has yet arrived. In this case
+A function that handles a command from Prooftree might fail
+because not all data from Prooftree has yet arrived. In this case
the continuation is stored in this variable and will be called
from `proof-tree-process-filter' when more output arrives.")
@@ -527,17 +527,17 @@ The command from prooftree has the form \"emacs exec: show-goal
"Add command `proof-tree-display-stop-command' to priority action list.
This function adds flag `'dont-show-when-silent' to the action
list item returned by `proof-tree-display-stop-command' and, when
-LAST-ITEM-FLAG is non-nil, also `'proof-tree-last-item'. The
+LAST-ITEM-FLAG is non-nil, also `'proof-tree-last-item'. The
former flag ensures that no show goals command is inserted after
`proof-tree-display-stop-command' when the prover runs completely
-silent. The latter flag serves as marker for
+silent. The latter flag serves as marker for
`proof-tree-check-proof-finish' that all requests from prooftree
-have been processed. The resulting action list item is added to
+have been processed. The resulting action list item is added to
`proof-priority-action-list'.
This function is called in 4 situations.
- A proof has been finished and the confirm-proof-complete
- message arrived from prooftree. Only in this case
+ message arrived from prooftree. Only in this case
LAST-ITEM-FLAG must be set.
- The user stopped the proof tree display inside Proof General.
- A stop-displaying message arrived, because the user stopped the
@@ -569,7 +569,7 @@ and switches the proof-tree display processing off."
(defun proof-tree-insert-output (string &optional message)
"Insert output or a message into the prooftree process buffer.
If MESSAGE is t, a message is inserted and
-`proof-tree-output-marker' is not touched. Otherwise, if
+`proof-tree-output-marker' is not touched. Otherwise, if
`proof-tree-output-marker' is nil, it is set to point to the
newly arrived output."
(with-current-buffer proof-tree-process-buffer
@@ -589,12 +589,12 @@ This function is the worker for `proof-tree-process-filter', it
implements all the functionality of `proof-tree-process-filter'.
Records the output in the prooftree process buffer and checks for
-callback function requests. Such callback functions might fail
+callback function requests. Such callback functions might fail
because the complete output from Prooftree has not arrived yet.
In this case they store a continuation function in
`proof-tree-filter-continuation that will be called when the next
-piece of output arrives. `proof-tree-output-marker' points to the
-next piece of Prooftree output that needs to get processed. If
+piece of output arrives. `proof-tree-output-marker' points to the
+next piece of Prooftree output that needs to get processed. If
everything is processed, the marker is deleted and
`proof-tree-insert-output' sets it again for the next output.
@@ -652,7 +652,7 @@ are transmitted atomically over a pipe."
(defun proof-tree-process-filter (_proc string)
"Output filter for prooftree.
This function is the exception wrapper, all the functionality is
-implemented in `proof-tree-process-filter-internal'. The filter
+implemented in `proof-tree-process-filter-internal'. The filter
records the output in `proof-tree-process-buffer' and calls
callback functions as necessary."
(condition-case err
@@ -665,7 +665,7 @@ callback functions as necessary."
;;
(defun proof-tree-process-sentinel (_proc event)
- "Sentinel for prooftee.
+ "Sentinel for prooftree.
Runs on process status changes and cleans up when prooftree dies."
(proof-tree-insert-output (concat "\nsubprocess status change: " event) t)
(unless (proof-tree-is-running)
@@ -863,7 +863,7 @@ lambda expressions that you can put into `proof-action-list'."
This function is for stopping the proof-tree display because of
some user request, which may either be an undo before the start
of the proof or some kind of quitting the proof-tree display in
-Proof General or in prooftree. In these cases no show-goal
+Proof General or in prooftree. In these cases no show-goal
commands need to be processed, therefore do not add the
`'proof-tree-last-item' flag to the stop command."
(setq proof-tree-current-proof nil)
@@ -879,9 +879,9 @@ line off for Coq) have been processed.
If this function detects the end of the proof, it moves
non-priority items following in `proof-action-list' to
`proof-tree--delayed-actions' and sets
-`proof-second-action-list-active'. When later the command from
+`proof-second-action-list-active'. When later the command from
`proof-tree-display-stop-command' is recognized, the items are
-moved back. If no items follow the end of the previous proof,
+moved back. If no items follow the end of the previous proof,
`proof-tree--delayed-actions' is set to t."
;; (message "PTCPF pt %s current %s mode %s delayed %s item %s"
;; proof-tree-current-proof (cadr (funcall proof-tree-get-proof-info))
@@ -921,12 +921,12 @@ moved back. If no items follow the end of the previous proof,
(defun proof-tree-urgent-action (last-item)
"Urgent actions for proof-tree display.
This is the second entry point of the Proof General prooftree support,
-see also `proof-tree-handle-delayed-output'. Call
+see also `proof-tree-handle-delayed-output'. Call
`proof-tree-check-proof-finish' to delay processing the queue region at
the end of a proof until all show-goal commands from prooftree have been
-processed. Do also call `proof-tree-assistant-specific-urgent-action',
+processed. Do also call `proof-tree-assistant-specific-urgent-action',
which appropriately inserts show-goal commands if Coq is running
-completely silent. LAST-ITEM is the last proof-action item that has just
+completely silent. LAST-ITEM is the last proof-action item that has just
been processed.
When the proof-tree display is active, this function is called from
@@ -966,8 +966,8 @@ current buffer."
This function cuts out the text between
`proof-tree-existentials-state-start-regexp' and
`proof-tree-existentials-state-end-regexp' from the prover
-output, including the matches of these regular expressions. If
-the start regexp is nil, the empty string is returned. If the end
+output, including the matches of these regular expressions. If
+the START regexp is nil, the empty string is returned. If the END
regexp is nil, the match expands to the end of the prover output."
(goto-char start)
(if (and proof-tree-existentials-state-start-regexp
@@ -985,9 +985,9 @@ regexp is nil, the match expands to the end of the prover output."
(defun proof-tree-handle-proof-progress (old-proof-marker cmd-string proof-info)
"Send CMD-STRING and goals in delayed output to prooftree.
This function is called if there is some real progress in a
-proof. This function sends the current state, the current goal
-and the list of additional open subgoals to Prooftree. Prooftree
-will sort out the rest. In particular, Prooftree determines
+proof. This function sends the current state, the current goal
+and the list of additional open subgoals to Prooftree. Prooftree
+will sort out the rest. In particular, Prooftree determines
without input from this function, whether or not a new layer in
the proof tree must be started.
@@ -1070,9 +1070,9 @@ The delayed output of the navigation command is in the region
"Callback to process a goal for prooftree.
This function should be used as callback for show-goal commands inserted
by `proof-tree-assistant-specific-urgent-action' for proof assistants
-running completely silent. OLD-ITEM should be the proof action list item
+running completely silent. OLD-ITEM should be the proof action list item
for which `proof-tree-assistant-specific-urgent-action' produced a show
-goal command. OLD-PROOF-INFO must be the result of
+goal command. OLD-PROOF-INFO must be the result of
`proof-tree-get-proof-info' just after old-item has been processed."
;; (message "PTDGC %s %s" old-item old-proof-info)
(with-current-buffer proof-shell-buffer
@@ -1109,7 +1109,7 @@ processing a show goal command might happen after the proof.
This function uses `proof-tree-update-goal-regexp' to find a
sequent, its ID and the corresponding state in the delayed
-output. If something is found an appropriate update-sequent
+output. If something is found an appropriate update-sequent
command is sent to prooftree.
The delayed output is in the region
@@ -1135,7 +1135,7 @@ The delayed output is in the region
(defun proof-tree-handle-delayed-output (old-proof-marker cmd flags _span)
"Process delayed output for prooftree.
This function is the main entry point of the Proof General prooftree
-support, but see also `proof-tree-urgent-action'. It examines the
+support, but see also `proof-tree-urgent-action'. It examines the
delayed output in order to take appropriate actions and maintains the
internal state.
@@ -1215,7 +1215,7 @@ the flags and SPAN is the span."
(defun proof-tree-display-current-proof (proof-start)
"Start an external proof-tree display for the current proof.
Coq (and probably other proof assistants as well) does not
-support outputing the current proof tree. Therefore this function
+support outputting the current proof tree. Therefore this function
retracts to the start of the current proof, switches the
proof-tree display on, and reasserts then until the former end of
the locked region. Argument PROOF-START must contain the start
diff --git a/generic/proof-unicode-tokens.el b/generic/proof-unicode-tokens.el
index 3702fd47d..66970ec68 100644
--- a/generic/proof-unicode-tokens.el
+++ b/generic/proof-unicode-tokens.el
@@ -69,7 +69,7 @@
;;;###autoload
(defun proof-unicode-tokens-set-global (flag)
- "Set global status of unicode tokens mode for PG buffers to be FLAG.
+ "Set global status of Unicode tokens mode for PG buffers to be FLAG.
Turn on/off menu in all script buffers and ensure new buffers follow suit."
(unless proof-unicode-tokens-initialised
(proof-unicode-tokens-init))
@@ -88,7 +88,7 @@ Turn on/off menu in all script buffers and ensure new buffers follow suit."
"Turn on or off Unicode tokens mode in Proof General script buffer.
This invokes `unicode-tokens-mode' to toggle the setting for the current
buffer, and then sets PG's option for default to match.
-Also we arrange to have unicode tokens mode turn itself on automatically
+Also we arrange to have Unicode tokens mode turn itself on automatically
in future if we have just activated it for this buffer.
Note: this function is called when the customize setting for the prover
is changed."
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index d14f29861..21d06f5a9 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -102,7 +102,7 @@ be inserted as the user types commands to the prover."
(defcustom proof-omit-proofs-option nil
"Set to t to omit complete opaque proofs for speed reasons.
When t, complete opaque proofs in the asserted region are not
-sent to the proof assistant (and thus not checked). For files
+sent to the proof assistant (and thus not checked). For files
with big proofs this can drastically reduce the processing time
for the asserted region at the cost of not checking the proofs.
For partial and non-opaque proofs in the asserted region all
@@ -263,11 +263,11 @@ selected frame will be automatically deleted."
(defcustom proof-shell-kill-function-also-kills-associated-buffers t
"*If non-nil, when `proof-shell-kill-function' is called, clean up buffers.
For example, `proof-shell-kill-function' is called when buffers
-are retracted when switching between proof script files. It may
-make sense to set this to `nil' when
+are retracted when switching between proof script files. It may
+make sense to set this to nil when
`proof-multiple-frames-enable' is set to prevent proof general
from killing frames that you want to be managed by a window
-manager instead of within emacs."
+manager instead of within Emacs."
:type 'boolean
:group 'proof-user-options)
@@ -381,7 +381,7 @@ One of the symbols: 'locked, 'follow, 'followdown, 'ignore.
If 'locked, point sticks to the end of the locked region.
If 'follow, point moves just when needed to display the locked region end.
-If 'followdown, point if necessary to stay in writeable region
+If 'followdown, point if necessary to stay in writable region
If 'ignore, point is never moved after movement commands or on errors.
If you choose 'ignore, you can find the end of the locked using
@@ -471,7 +471,7 @@ regions of the script."
(defcustom proof-minibuffer-messages nil
"*Non-nil causes Proof General to issue minibuffer messages.
-Minibuffer messages are issed when urgent messages are seen
+Minibuffer messages are issued when urgent messages are seen
from the prover. You can disable the display of these if they
are distracting or too frequent."
:type 'boolean
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index 1e0f40798..1d05730f3 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -189,7 +189,7 @@ Restrict to BUFLIST if it's set."
"Prevent this associated buffer from being killed: merely erase it.
A hook function for `kill-buffer-hook'.
This is a fairly crude and not-entirely-robust way to prevent the
-user accidently killing an associated buffer."
+user accidentally killing an associated buffer."
(if (and (proof-shell-live-buffer) proof-buffer-type)
(progn
(let ((bufname (buffer-name)))
diff --git a/lib/bufhist.el b/lib/bufhist.el
index d7cce2d4f..72a2f318b 100644
--- a/lib/bufhist.el
+++ b/lib/bufhist.el
@@ -55,7 +55,7 @@
;;; Now our code
(defgroup bufhist nil
- "In-memory history of buffer contents"
+ "In-memory history of buffer contents."
:group 'tools)
(defcustom bufhist-ring-size 30
@@ -81,7 +81,7 @@
"Ordinary value `buffer-read-only' for this buffer.")
(defvar bufhist-top-point 0
- "Poistion of top of real buffer contents, after buttons.")
+ "Position of top of real buffer contents, after buttons.")
(defun bufhist-mode-line-format-entry ()
(when bufhist-ring-pos
@@ -167,7 +167,7 @@ This is as a pair (POINT . CONTENTS)."
(goto-char (car buf)))
(defun bufhist-checkpoint ()
- "Add buffer contents to the ring history. No action if not in bufhist mode."
+ "Add buffer contents to the ring history. No action if not in `bufhist-mode'."
(interactive)
(if bufhist-mode ;; safety
(ring-insert bufhist-ring (bufhist-get-buffer-contents))))
@@ -186,7 +186,7 @@ This is as a pair (POINT . CONTENTS)."
(defun bufhist-checkpoint-and-erase ()
"Add buffer contents to history then erase.
-Only erase if not in bufhist mode."
+Only erase if not in `bufhist-mode'."
(interactive)
(bufhist-checkpoint)
(bufhist-erase-buffer))
@@ -283,7 +283,7 @@ If N is omitted or nil, move forward by one item."
;;;###autoload
(defun bufhist-init (&optional readwrite ringsize)
- "Initialise a ring history for the current buffer.
+ "Initialize a ring history for the current buffer.
The history will be read-only unless READWRITE is non-nil.
For read-only histories, edits to the buffer switch to the latest version.
If RINGSIZE is omitted or nil, the size defaults to ‘bufhist-ring-size’."
diff --git a/lib/holes.el b/lib/holes.el
index 80c23c844..4a0f1d01d 100644
--- a/lib/holes.el
+++ b/lib/holes.el
@@ -168,15 +168,15 @@ This is not the keymap used on holes's overlay (see `hole-map' instead).")
;;;
(defun holes-region-beginning-or-nil ()
- "Return the beginning of the acitve region, or nil."
+ "Return the beginning of the active region, or nil."
(and mark-active (region-beginning)))
(defun holes-region-end-or-nil ()
- "Return the end of the acitve region, or nil."
+ "Return the end of the active region, or nil."
(and mark-active (region-end)))
(defun holes-copy-active-region ()
- "Copy and retuurn the active region."
+ "Copy and return the active region."
(cl-assert mark-active nil "the region is not active now.")
(copy-region-as-kill (region-beginning) (region-end))
(car kill-ring))
@@ -347,7 +347,7 @@ Operate between character positions FROM and TO."
(defun holes-clear-all-buffer-holes (&optional start end)
"Clear all holes leaving their contents.
-Operate betwenn START and END if non nil."
+Operate between START and END if non nil."
(interactive)
(holes-disable-active-hole)
(span-mapcar-spans
@@ -452,7 +452,7 @@ following hole if it exists."
(setq holes-active-hole holes-default-hole)))))
(defun holes-delete-update-active-hole ()
- "Deletes the active hole and supresses its content.
+ "Deletes the active hole and suppresses its content.
Sets `holes-active-hole' to the next hole if it exists."
(interactive)
(holes-replace-update-active-hole ""))
@@ -642,7 +642,7 @@ With arg, turn Outline minor mode on if arg is positive, off otherwise.
The mode `holes-mode' is meant to help program editing. It is
useful to build complicated expressions by copy pasting several
-peices of text from different parts of a buffer (or even from
+pieces of text from different parts of a buffer (or even from
different buffers).
HOLES
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 8b5be2a31..247250651 100644
--- a/lib/local-vars-list.el
+++ b/lib/local-vars-list.el
@@ -49,7 +49,7 @@ local-vars-list provides two useful functions:
(defun local-vars-list-find ()
"Find the local variable definition paragraph.
Return a list containing the prefix and the suffix of its first line,
-or throw 'notfound if not found. Sets the point at the beginning of
+or throw 'notfound if not found. Sets the point at the beginning of
the second line of the paragraph."
(goto-char (point-max))
(catch 'notfound
@@ -113,12 +113,12 @@ variable definition (or at the \"End:\" line)."
;; Only looks for file local vars. Not dir local vars.
(defun local-vars-list-get (symb)
- "Return the value written in the local variable list for variable symb.
+ "Return the value written in the local variable list for variable SYMB.
Raises an error if symb is not in the list.
Note: Using `file-local-variables-alist' is not comfortable here
since editing by hand the file variable zone does not modify this
-alist. Proceed by looking in the file instead."
+alist. Proceed by looking in the file instead."
(save-excursion
(let*
((lrpat (local-vars-list-find))
@@ -134,14 +134,13 @@ alist. Proceed by looking in the file instead."
(local-vars-list-get-current lpat rpat))))
(defun local-vars-list-get-safe (symb)
- "Return true if variable SYMB belongs to the local variable list of the
-current buffer."
+ "Non-nil if SYMB belongs to the local variable list of the current buffer."
(condition-case nil (local-vars-list-get symb) (error nil)))
(defun local-vars-list-set (symb val)
- "Write the value val in the local variable list for variable symb.
+ "Write the value VAL in the local variable list for variable SYMB.
If the variable is already specified in the list, replace the
-value. If no local variable list is found, create one at the end
+value. If no local variable list is found, create one at the end
of the buffer first."
(add-file-local-variable symb val))
diff --git a/lib/maths-menu.el b/lib/maths-menu.el
index ab61f8a3a..c89d26af9 100644
--- a/lib/maths-menu.el
+++ b/lib/maths-menu.el
@@ -354,7 +354,7 @@
(define-minor-mode maths-menu-mode
"Install a menu for entering mathematical characters.
Uses window system menus only when they can display multilingual text.
-Otherwise the menu-bar item activates the text-mode menu system.
+Otherwise the menu-bar item activates the `text-mode' menu system.
This mode is only useful with a font which can display the maths repertoire."
:lighter nil)
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index 11fdada1e..b1b3c8ae3 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -41,7 +41,7 @@
;;
;; -- insert tokens via numeric code (extra format string), cf HTML
;; -- simplify: unify region and control settings?
-;; -- simplify/optimise property handling
+;; -- simplify/optimize property handling
;; -- support multiple modes with mode-local configs at once
;;; Code:
@@ -123,10 +123,10 @@ the longer text, if any.
If set, this variable is used instead of `unicode-tokens-token-format'.")
(defvar unicode-tokens-shortcut-alist nil
- "An alist of keyboard shortcuts to unicode strings.
+ "An alist of keyboard shortcuts to Unicode strings.
The alist is added to the input mode for tokens.
The shortcuts are only used for input convenience; no reverse
-mapping back to shortucts is performed. Behaviour is like abbrev.")
+mapping back to shortcuts is performed. Behaviour is like abbrev.")
(defvar unicode-tokens-shortcut-replacement-alist nil
"Overrides `unicode-tokens-shortcut-alist'.
@@ -139,14 +139,14 @@ Used for `unicode-tokens-replace-shortcuts'.")
(defvar unicode-tokens-control-region-format-regexp nil
"A regexp for control regions, with up to two %s placeholders.
-When fomatted with arguments START END, results in a regexp
+When formatted with arguments START END, results in a regexp
that matches a control region. There should be three delimited
subexpressions: (match-string 1) and (match-string 3) are hidden,
and (match-string 2) has the display control applied.")
(defvar unicode-tokens-control-char-format-regexp nil
"A format string for control characters, possibly with a %s placeholder.
-When fomatted with arguments STRING, results in a regexp
+When formatted with arguments STRING, results in a regexp
that matches a control character sequence. There should be two
delimited subexpressions: (match-string 1) is hidden
and (match-string 2) has the display control applied.")
@@ -161,7 +161,7 @@ and (match-string 2) has the display control applied.")
"A format string for inserting a control character sequence.")
(defvar unicode-tokens-control-region-format-start nil
- "A format string for begining a control region sequence.")
+ "A format string for beginning a control region sequence.")
(defvar unicode-tokens-control-region-format-end nil
"A format string for ending a control region sequence.")
@@ -247,7 +247,7 @@ span the token name, if that is shorter.
The value is calculated by `unicode-tokens-calculate-token-match'.")
(defvar unicode-tokens-uchar-hash-table nil
- "Hash table mapping unicode strings to symbolic token names.
+ "Hash table mapping Unicode strings to symbolic token names.
This is used for an approximate reverse mapping, see `unicode-tokens-paste'.")
(defvar unicode-tokens-uchar-regexp nil
@@ -505,7 +505,7 @@ The check is with `char-displayable-p'."
Regexp match data number MATCH selects the token name, while match
number 1 matches the text to be replaced.
Token name from MATCH is searched for in `unicode-tokens-hash-table'.
-The face property is set to the :family and :slant attriubutes taken from
+The face property is set to the :family and :slant attributes taken from
`unicode-tokens-symbol-font-face'."
(let* ((start (match-beginning 0))
(end (match-end 0))
@@ -608,7 +608,7 @@ Optional argument FACENIL means set the face property to nil, unless 'face is in
;;
(defvar unicode-tokens-show-controls nil
- "Non-nil supresses hiding of control tokens.")
+ "Non-nil suppresses hiding of control tokens.")
(defun unicode-tokens-show-controls (&optional arg)
"Toggle variable `unicode-tokens-show-controls'. With ARG, turn on iff positive."
@@ -888,7 +888,7 @@ Starts from point."
(format unicode-tokens-token-format token)))))
(defun unicode-tokens-replace-unicode ()
- "Query-replace unicode seq. in the buffer with tokens having same appearance.
+ "Query-replace Unicode seq. in the buffer with tokens having same appearance.
Starts from point."
(interactive)
(let ((uchar-regexp unicode-tokens-uchar-regexp))
@@ -995,13 +995,13 @@ Starts from point."
(funcall fn (point-min) (point-max))))
(defun unicode-tokens-encode (beg end)
- "Return a unicode encoded version of the presentation in region BEG..END."
+ "Return a Unicode encoded version of the presentation in region BEG..END."
(unicode-tokens-encode-in-temp-buffer
(buffer-substring-no-properties beg end) 'buffer-substring))
;;;###autoload
(defun unicode-tokens-encode-str (str)
- "Return a unicode encoded version presentation of STR."
+ "Return a Unicode encoded version presentation of STR."
(unicode-tokens-encode-in-temp-buffer str 'buffer-substring))
(defun unicode-tokens-copy (beg end)
@@ -1040,7 +1040,7 @@ of symbol compositions, and will lose layout information."
"Font lock patterns for highlighting Unicode tokens.")
(defun unicode-tokens-highlight-unicode ()
- "Hilight Unicode characters in the buffer.
+ "Highlight Unicode characters in the buffer.
Toggles highlighting of Unicode characters used in the
buffer beyond the legacy 8-bit character set codes. This is
useful to manually determine if a buffer contains Unicode or
@@ -1066,7 +1066,7 @@ tokenised symbols."
;;
(defun unicode-tokens-initialise ()
- "Perform initialisation for Unicode Tokens minor mode.
+ "Perform initialization for Unicode Tokens minor mode.
This function calculates `font-lock-keywords' and other configuration
variables."
(interactive)
@@ -1102,7 +1102,7 @@ positive, otherwise turn it off.
In Unicode Tokens mode (Utoks appears in the modeline), a
sequence of characters in the buffer (a token) may be presented
-instead as a Unicode character. The underlying buffer contents is
+instead as a Unicode character. The underlying buffer contents is
not changed, only what is presented on the display. Other tokens
may be used to control layout, for example, enabling sub/super
scripts, bold and italic fonts, etc. Keyboard shortcut sequences
diff --git a/obsolete/demoisa/demoisa.el b/obsolete/demoisa/demoisa.el
index 895b32822..aa4bcf76e 100644
--- a/obsolete/demoisa/demoisa.el
+++ b/obsolete/demoisa/demoisa.el
@@ -1,4 +1,4 @@
-;; demoisa.el Example Proof General instance for Isabelle
+;;; demoisa.el --- Example Proof General instance for Isabelle
;;
;; Copyright (C) 1999 LFCS Edinburgh.
;;
@@ -6,7 +6,8 @@
;;
;; $Id$
;;
-;; =================================================================
+
+;;; Commentary:
;;
;; See README in this directory for an introduction.
;;
@@ -30,6 +31,8 @@
;; shell before starting Emacs (or customize proof-assistants).
;;
+;;; Code:
+
(require 'proof) ; load generic parts
(require 'pg-goals)
(require 'pg-response)
@@ -138,3 +141,5 @@
;; configuration for the goals buffer.
(provide 'demoisa)
+
+;;; demoisa.el ends here
diff --git a/phox/phox.el b/phox/phox.el
index 375272dec..81ccb2b77 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -121,8 +121,7 @@ version of it in Phox code, with no chars in [a-z0-9A-Z] after it."
;;Goto http://www.fileformat.info/info/unicode/block/mathematical_operators/list.htm and copy the needed character
(defun phox-unicode-simplified ()
- "Adds a bunch of font-lock rules to display phox commands as
-their unicode counterpart"
+ "Adds font-lock rules to display Phox commands as their Unicode counterpart."
(interactive)
(substitute-patterns-with-unicode-symbol
(list
diff --git a/qrhl/qrhl.el b/qrhl/qrhl.el
index d67c57541..283022894 100644
--- a/qrhl/qrhl.el
+++ b/qrhl/qrhl.el
@@ -21,15 +21,15 @@
(defcustom qrhl-input-method "qrhl"
- "Input method to use when editing qRHL proof scripts"
+ "Input method to use when editing qRHL proof scripts."
:type '(string) :group 'qrhl)
(defcustom qrhl-prog-name "qrhl"
- "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)"
+ "Name/path of the qrhl-prover command. (Restart Emacs after changing this.)."
:type '(string) :group 'qrhl)
(defcustom qrhl-indentation-level 2
- "Indentation level in qRHL scripts"
+ "Indentation level in qRHL scripts."
:group 'qrhl)
(defun qrhl-find-and-forget (span)
@@ -46,7 +46,7 @@
focus-cmd))
(defun qrhl-forward-regex (regex)
- "If text starting at point matches REGEX, move to end of the match and return t.
+ "If text starting at point matches REGEX, move to end of the match and return t.
Otherwise return nil"
(and (looking-at regex) (goto-char (match-end 0)) t))
@@ -71,7 +71,7 @@ Returns t if this worked."
(goto-char (match-end 0))))
(defun qrhl-proof-script-parse-function ()
- "Finds the command/comment starting at the point"
+ "Finds the command/comment starting at the point."
(or (and (qrhl-forward-regex "#[^\n]*\n") 'comment)
(and (qrhl-parse-focus-command) 'cmd)
(and (qrhl-parse-regular-command) 'cmd)))
@@ -83,7 +83,7 @@ Returns t if this worked."
("\\(⇧\\)\\([^⇩⇧[:space:]]\\)" .
((2 '(face superscript display (raise 0.3)))
(1 '(face nil display "")))))
- "Font-lock configuration for displaying sub/superscripts that are prefixed by ⇩/⇧")
+ "Font-lock configuration for displaying sub/superscripts that are prefixed by ⇩/⇧.")
(defvar qrhl-font-lock-keywords
; Regexp explanation: match the keyword/tactic after another command, and also if there are {}+*- in between (focusing commands)
@@ -103,7 +103,7 @@ Returns t if this worked."
; Regexp explanation: Match comment after
'(("\\(?:^\\|[ \t]\\)[ \t]*\\(#.*\\)" . (1 'font-lock-comment-face)))
))
- "Font-lock configuration for qRHL proof scripts")
+ "Font-lock configuration for qRHL proof scripts.")
(defun qrhl-proof-script-preprocess (file start end cmd)
"Strips comments from the command CMD.
@@ -152,7 +152,7 @@ Called before sending CMD to the prover."
(find-file (buffer-substring (button-start button) (button-end button))))
(defun qrhl-buttonize-buffer ()
- "Turn all include commands in a qRHL proof script into clickable buttons"
+ "Turn all include commands in a qRHL proof script into clickable buttons."
(interactive)
(remove-overlays)
(save-excursion
@@ -163,8 +163,8 @@ Called before sending CMD to the prover."
(defun qrhl-current-line-rel-indent ()
- "Determins by how much to indent the current line relative to the previous
- indentation level. (Taking into account only the current line.)"
+ "Determines by how much to indent the current line relative to the previous
+indentation level. (Taking into account only the current line.)"
(save-excursion
(let ((qrhl-qed-pattern "^[ \t]*qed\\b")
(closing-brace-pattern "^[ \t]*}"))
@@ -179,7 +179,7 @@ Called before sending CMD to the prover."
(t 0)))))
(defun qrhl-indent-line ()
- "Indent current line as qRHL proof script"
+ "Indent current line as qRHL proof script."
(interactive)
(let ((not-found t) (previous-indent nil) (previous-offset 0) rel-indent
@@ -237,3 +237,5 @@ Called before sending CMD to the prover."
(qrhl-buttonize-buffer)))
(provide 'qrhl)
+
+;;; qrhl.el ends here
diff --git a/resources/checkdoc-config.el b/resources/checkdoc-config.el
new file mode 100644
index 000000000..569036601
--- /dev/null
+++ b/resources/checkdoc-config.el
@@ -0,0 +1,287 @@
+;;; checkdoc-config.el --- Configuration for running checkdoc -*- lexical-binding: t; -*-
+
+;; This file is part of Proof General.
+
+;; The software is free software: you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation, either version 3 of the License, or
+;; (at your option) any later version.
+
+;; This program is distributed in the hope that it will be useful,
+;; but WITHOUT ANY WARRANTY; without even the implied warranty of
+;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
+;; GNU General Public License for more details.
+
+;; You should have received a copy of the GNU General Public License
+;; along with this program. If not, see .
+
+;;; Commentary:
+
+;;; Code:
+
+(defvar checkdoc-package-keywords-flag)
+(defvar checkdoc-spellcheck-documentation-flag)
+(defvar checkdoc-ispell-lisp-words)
+
+(with-eval-after-load "checkdoc"
+
+ ;; Output file names relative to the root directory
+ (advice-add 'checkdoc-buffer-label :around
+ (lambda (fun)
+ (let ((default-directory (locate-dominating-file default-directory ".git")))
+ (funcall fun))))
+
+ ;; Things to fix eventually
+ (setq checkdoc-force-docstrings-flag nil)
+ (setq checkdoc--interactive-docstring-flag nil)
+ (setq checkdoc-arguments-missing-flag nil)
+
+ (setq checkdoc-package-keywords-flag t)
+ (setq checkdoc-spellcheck-documentation-flag t)
+ (setq checkdoc-ispell-lisp-words
+
+ '(;; default value of `checkdoc-ispell-lisp-words'
+ "alist" "emacs" "etags" "keymap" "paren" "regexp" "sexp"
+
+ "BackTo"
+ "CompCert"
+ "CoqProject"
+ "EasyCrypt"
+ "Imenu"
+ "LoadPath"
+ "PROJECT's"
+ "Phox"
+ "ProofGeneral"
+ "Qed"
+ "RightClick"
+ "Rocq"
+ "RocqProject"
+ "SComint"
+ "Toplevel"
+ "UTF"
+ "aN"
+ "addids"
+ "alreadyopen"
+ "analyse"
+ "analysed"
+ "arg"
+ "args"
+ "askids"
+ "askpgip"
+ "askprefs"
+ "async"
+ "autodetected"
+ "autosend"
+ "backend"
+ "basename"
+ "beghypname"
+ "behaviour"
+ "bigjobs"
+ "browsable"
+ "buf"
+ "bufhist"
+ "canonicalized"
+ "cmd"
+ "colour"
+ "coloured"
+ "colouring"
+ "comint"
+ "concl"
+ "config"
+ "containt"
+ "coq"
+ "coqc"
+ "coqdep"
+ "coqtop"
+ "ctrl"
+ "curlies"
+ "customizable"
+ "customizations"
+ "cygwin"
+ "deffn"
+ "defopt"
+ "defs"
+ "delids"
+ "dep"
+ "dependee"
+ "dependees"
+ "descr"
+ "desynchronized"
+ "dir"
+ "docstring"
+ "docstrings"
+ "el"
+ "elisp"
+ "elts"
+ "endhypname"
+ "env"
+ "eval"
+ "evar"
+ "evars"
+ "exe"
+ "exec'd"
+ "existentials"
+ "facename"
+ "favourite"
+ "favourites"
+ "filestatus"
+ "fixpoint"
+ "floatset"
+ "fontify"
+ "fontifying"
+ "fontset"
+ "fontsets"
+ "forall"
+ "fraktur"
+ "github"
+ "glyphs"
+ "goalsave"
+ "goto"
+ "haspref"
+ "holes's"
+ "https"
+ "hyp"
+ "hypcrossov"
+ "hypname"
+ "hypnameov"
+ "hyps"
+ "ident"
+ "idn"
+ "idtables"
+ "ifb"
+ "iff"
+ "infoH"
+ "infos"
+ "init"
+ "initialise"
+ "initialised"
+ "initialises"
+ "instantiation"
+ "instantiations"
+ "intitalizes"
+ "ints"
+ "intset"
+ "invariants"
+ "isar"
+ "iteratively"
+ "ith"
+ "keydef"
+ "keymaps"
+ "loopbacks"
+ "lpat"
+ "ltac"
+ "makefile"
+ "massb"
+ "matcher"
+ "maths"
+ "minibuffer"
+ "modeline"
+ "monadic"
+ "munge"
+ "myassert"
+ "mytac"
+ "nat"
+ "nd"
+ "newfile"
+ "nonrecursive"
+ "opam"
+ "pbp"
+ "pbrpm"
+ "personalization"
+ "pgdynamic"
+ "pggroup"
+ "pgip"
+ "pgipgcmd"
+ "pgiptype"
+ "pico"
+ "plist"
+ "pos"
+ "pre"
+ "precomputed"
+ "prepended"
+ "prev"
+ "prog"
+ "proofer"
+ "proofstart"
+ "proofstate"
+ "prooftree"
+ "prover"
+ "prover's"
+ "proverid"
+ "provers"
+ "ptys"
+ "qRHL"
+ "qed"
+ "qualid"
+ "recompilations"
+ "recureses"
+ "recurse"
+ "redisplayed"
+ "rehighlight"
+ "rehighlighted"
+ "reinitialise"
+ "reparse"
+ "resynchronised"
+ "rpat"
+ "savegoal"
+ "sequent"
+ "serie"
+ "setids"
+ "sexp"
+ "sexps"
+ "smie"
+ "src"
+ "srcid"
+ "srcrds"
+ "standardly"
+ "stderr"
+ "stdout"
+ "stepwise"
+ "stm"
+ "str"
+ "struct"
+ "subdirectory"
+ "subexpr"
+ "subexpressions"
+ "subgoal"
+ "subgoals"
+ "sublist"
+ "submenu"
+ "submenus"
+ "substring"
+ "substrings"
+ "subterm"
+ "subtree"
+ "symb"
+ "tac"
+ "tacticals"
+ "texi"
+ "thm"
+ "tokenised"
+ "toolchain"
+ "tooltip"
+ "tooltips"
+ "topfile"
+ "truename"
+ "unadjusted"
+ "unclosed"
+ "undoable"
+ "undos"
+ "unfocusing"
+ "unfontify"
+ "unhighlight"
+ "uninstantiated"
+ "uninterned"
+ "unsets"
+ "util"
+ "vio"
+ "vo"
+ "vok"
+ "vos"
+ "wellformedness"
+ "whitespace"
+ "xml")))
+
+(provide 'checkdoc-config)
+
+;;; checkdoc-config.el ends here