branch: elpa/proof-general
commit 63d9f75db5bfb89d7d6feed30dfaa895ce9a94c8
Author: Morgan Smith <[email protected]>
Commit: Morgan Smith <[email protected]>
Fix wrong usage of unescaped single quotes in docstrings
On modern Emacsen this is a compile time warning. Before this change there
where 111 of these warnings. Now there are 7.
---
ci/compile-tests/007-slow-require/runtest.el | 2 +-
ci/compile-tests/cct-lib.el | 8 +-
coq/coq-par-compile.el | 116 +++++++++++++--------------
coq/coq-seq-compile.el | 10 +--
coq/coq-smie.el | 2 +-
coq/coq-system.el | 12 +--
coq/coq.el | 20 ++---
generic/pg-autotest.el | 4 +-
generic/pg-pamacs.el | 6 +-
generic/pg-response.el | 12 +--
generic/pg-user.el | 20 ++---
generic/pg-vars.el | 16 ++--
generic/proof-config.el | 38 ++++-----
generic/proof-script.el | 64 +++++++--------
generic/proof-shell.el | 42 +++++-----
generic/proof-syntax.el | 2 +-
generic/proof-tree.el | 6 +-
generic/proof-useropts.el | 32 ++++----
lib/local-vars-list.el | 2 +-
lib/span.el | 4 +-
lib/unicode-tokens.el | 2 +-
21 files changed, 210 insertions(+), 210 deletions(-)
diff --git a/ci/compile-tests/007-slow-require/runtest.el
b/ci/compile-tests/007-slow-require/runtest.el
index 9d7ee38bfe5..e2f7b7a6ae6 100644
--- a/ci/compile-tests/007-slow-require/runtest.el
+++ b/ci/compile-tests/007-slow-require/runtest.el
@@ -112,7 +112,7 @@ See `cct-generic-check-main-buffer'."
(defun test-slow-require (n)
"Test part N of slow require job tests.
XXX Test a setting where the second require job is still in state
-'enqueued-coqdep when the first one finishes."
+\\+`enqueued-coqdep' when the first one finishes."
(let*
;; .v file names are used as file and as buffer names
((av (format "a%d.v" n))
diff --git a/ci/compile-tests/cct-lib.el b/ci/compile-tests/cct-lib.el
index a6df5813def..f249263faf3 100644
--- a/ci/compile-tests/cct-lib.el
+++ b/ci/compile-tests/cct-lib.el
@@ -165,7 +165,7 @@ Runs `cct-before-busy-waiting-hook' and
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
-vanilla (stored at 'type in the span property list) are created
+vanilla (stored at \\+`type' in the span property list) are created
for real commands (not for comments). They hold various
information that is used, among others, for backtracking.
@@ -188,7 +188,7 @@ and `current-message' does not return anything."
(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
+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)))
@@ -219,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"
@@ -236,7 +236,7 @@ list of file names."
The comparison treats ANCESTORS as set but the file names must
be `equal' as strings.
-Ancestors are recorded 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
diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el
index 227589143f0..967b234a1e3 100644
--- a/coq/coq-par-compile.el
+++ b/coq/coq-par-compile.el
@@ -519,7 +519,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,
-see `current-time') or the symbol 'just-compiled, where the
+see `current-time') or the symbol \\+`just-compiled', where the
latter is greater then everything else."
(cond
((eq time-2 'just-compiled) t)
@@ -683,7 +683,7 @@ Use `coq-par-second-stage-enqueue',
"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
-'enqueue-coqc can be ignored, because they can never participate
+\\+`enqueue-coqc' can be ignored, because they can never participate
in a cycle."
;; CORRECTNESS ARGUMENT FOR THIS FUNCTION
;;
@@ -736,9 +736,9 @@ in a cycle."
cycle)))
(defun coq-par-find-dependency-circle ()
- "Find a dependency cycle in compilation jobs of state 'waiting-dep.
+ "Find a dependency cycle in compilation jobs of state \\+`waiting-dep'.
If no circle is found return nil, otherwise the list of files
-belonging to the circle. Jobs in state 'enqueue-coqc can be
+belonging to the circle. Jobs in state \\+`enqueue-coqc' can be
ignored, because they can never participate in a cycle."
(let (cycle)
(maphash (lambda (_key job) (put job 'visited nil))
@@ -1007,7 +1007,7 @@ determines the exit status and calls the continuation
function
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
-jobs are done with the 'script-buf as current buffer, such that
+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
@@ -1105,7 +1105,7 @@ function and reported appropriately."
(defun coq-par-run-second-stage-queue ()
"Start delayed second stage compilation (vio2vo or vok).
-Use the buffer stored in the 'script-buf property as current
+Use the buffer stored in the \\+`script-buf' property as current
buffer for starting processes, such that local variables and, in
particular, `default-directory' have the correct values."
;; when the user starts another compilation, the timer for second
@@ -1199,17 +1199,17 @@ Therefore DEPENDANT must wait for DEPENDEE to finish."
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
+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
+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.
+\\+`obj-mod-time' remembers the time stamp of \\+`required-obj-file'.
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
-'second-stage property on job if necessary."
+\\+`second-stage' property on job if necessary."
(let* ((vo-file (get job 'vo-file))
(vio-file (coq-library-vio-of-vo-file vo-file))
(vo-obj-time (nth 5 (file-attributes vo-file)))
@@ -1374,11 +1374,11 @@ 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
-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
+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
the .vos or .vo file, depending on `coq-compile-prefer-vos'. Sets
-the 'second-stage property on job to 'vok if necessary."
+the \\+`second-stage' property on job to \\+`vok' if necessary."
(let* ((vo-file (get job 'vo-file))
(vos-file (coq-library-vos-of-vo-file vo-file))
(dep-time (get job 'youngest-coqc-dependency))
@@ -1451,10 +1451,10 @@ the 'second-stage property on job to 'vok if necessary."
"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
+t if a compilation is required and sets the \\+`use-quick' property
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 compilation is needed, \\+`required-obj-file' is set. Property
+\\+`obj-mod-time' is set when no compilation is needed."
(if (coq--post-v811)
(coq-par-job-needs-compilation-vos job)
(coq-par-job-needs-compilation-quick job)))
@@ -1465,7 +1465,7 @@ 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
-'collect-visited property on all returned jobs, which should be
+\\+`collect-visited' property on all returned jobs, which should be
cleared before the next collection run."
;; (message "CLAD: job %s: dependees %s"
;; (get job 'name)
@@ -1480,7 +1480,7 @@ cleared before the next collection run."
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
-sets the 'collect-visited property on all returned jobs, which
+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"
;; (get job 'name) (get job 'collect-visited) (get job 'lock-state))
@@ -1514,7 +1514,7 @@ 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
+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
collection, such that its use stays internal."
@@ -1533,9 +1533,9 @@ collection, such that its use stays internal."
JOB must be a successful require job.
This function performs the essential tasks for successful require
-jobs when they transition from 'waiting-queue to 'ready:
+jobs when they transition from \\+`waiting-queue' to \\+`ready':
- Registering ancestors in the span and recording this fact in
- the 'lock-state property.
+ the \\+`lock-state' property.
- Moving queue items back to `proof-action-list' and start their
execution.
- Insert `coq-par-require-processed' as callback if this is the
@@ -1597,27 +1597,27 @@ used to enter background compilation functions from
(coq-par-kickoff-queue-maybe job)))
(defun coq-par-kickoff-queue-maybe (job)
- "Transition require job JOB to 'waiting-queue and maybe to 'ready.
+ "Transition require job JOB to \\+`waiting-queue' and maybe to \\+`ready'.
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
+must not be called if JOB is in state \\+`enqueued-coqdep' or in
+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).
+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
+ \\+`queue-span' and marked as \\+`asserted' in their \\+`lock-state'
property
-- processing of items in 'queueitems is started (if JOB is successful)
+- processing of items in \\+`queueitems' is started (if JOB is successful)
- a possible queue dependent gets it's dependency cleared, and,
- if possible the 'waiting-queue -> 'ready transition
+ if possible the \\+`waiting-queue' -> \\+`ready' transition
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
@@ -1730,15 +1730,15 @@ 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
+First JOB is put into state \\+`enqueued-coqc'. Then it is determined
if JOB needs compilation, what file must be produced (depending
on `coq-compile-quick') and if a .vio or .vo file must be
deleted. If necessary, deletion happens immediately. If JOB needs
compilation, compilation is started or the JOB is enqueued and
-JOB stays in 'enqueued-coqc for the time being. Otherwise, the
-transition 'enqueued-coqc -> 'ready is triggered."
+JOB stays in \\+`enqueued-coqc' for the time being. Otherwise, the
+transition \\+`enqueued-coqc' -> \\+`ready' is triggered."
(cl-assert (eq (get job 'type) 'file)
nil "wrong job type in coq-par-compile-job-maybe")
(put job 'state 'enqueued-coqc)
@@ -1761,14 +1761,14 @@ transition 'enqueued-coqc -> 'ready is triggered."
"Clear Coq dependency and update dependee information in DEPENDANT.
This function handles a Coq dependency from child dependee to
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
+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
-time or 'just-compiled. The dependency
+time or \\+`just-compiled'. The dependency
count of DEPENDANT is decreased and, if it reaches 0, the next
-transition is triggered for DEPENDANT. For 'file jobs this is
-'waiting-dep -> 'enqueued-coqc and for 'require jobs this is
-'waiting-dep -> 'waiting-queue.
+transition is triggered for DEPENDANT. For \\+`file' jobs this is
+\\+`waiting-dep' -> \\+`enqueued-coqc' and for \\+`require' jobs this is
+\\+`waiting-dep' -> \\+`waiting-queue'.
This function must be called for failed jobs to complete all
necessary transitions."
@@ -1791,23 +1791,23 @@ necessary transitions."
(coq-par-kickoff-queue-maybe dependant))))
(defun coq-par-kickoff-coqc-dependants (job just-compiled)
- "Handle transition to state 'ready for file job JOB.
+ "Handle transition to state \\+`ready' for file job JOB.
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
-function sets 'youngest-coqc-dependency to the maximal (youngest)
+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
-dependents, propagates 'youngest-coqc-dependency and
+dependents, propagates \\+`youngest-coqc-dependency' and
starts any necessary state transitions on the
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
-failed, this function relies on 'obj-mod-time has been set
+failed, this function relies on \\+`obj-mod-time' has been set
before."
(cl-assert (not (eq (get job 'type) 'require))
nil "kickoff-coqc-dependants called for require job")
@@ -1908,7 +1908,7 @@ Lock the source file and start the coqdep background
process."
(defun coq-par-start-coqc (job)
"Start coqc background compilation for JOB.
-Depending on property 'use-quick, vos or quick compilation may be
+Depending on property \\+`use-quick', vos or quick compilation may be
used."
(message "Recompile %s%s"
(cond
@@ -2025,7 +2025,7 @@ synchronously or asynchronously."
(coq-par-job-enqueue new-job)))
(defun coq-par-job-init-common (clpath type script-buf)
- "Common initialization for 'require and 'file jobs.
+ "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
@@ -2053,7 +2053,7 @@ 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
+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.
@@ -2088,7 +2088,7 @@ 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
-particular, initialize its 'lock-state property from the set of
+particular, initialize its \\+`lock-state' property from the set of
as locked registered files in `proof-included-files-list'.
If a new job is created it is started or enqueued right away."
@@ -2123,8 +2123,8 @@ 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 dependents with 'failed.
-Mark JOB with 'failed and unlock ancestors as appropriate.
+ "Mark require JOB and its queue dependents with \\+`failed'.
+Mark JOB with \\+`failed' and unlock ancestors as appropriate.
Recurse for queue dependents."
(unless (get job 'failed)
(put job 'failed t)
@@ -2137,7 +2137,7 @@ Recurse for queue dependents."
(defun coq-par-mark-job-failing (job)
"Mark all dependents of JOB as failing and unlock ancestors as appropriate.
-Set the 'failed property on all direct and indirect dependents of
+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)
@@ -2156,16 +2156,16 @@ error, the job is marked as failed or compilation is
aborted via
a signal (depending on `coq-compile-keep-going'). If there was no
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
+- 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
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
- 'enqueued-coqc, for require jobs it goes to 'waiting-queue.
+ \\+`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.
@@ -2236,9 +2236,9 @@ is directly passed to `coq-par-analyse-coq-dep-exit'."
(defun coq-par-coqc-continuation (process exit-status)
"Coqc continuation function.
-If coqc failed, signal an error or mark the job as 'failed, and
+If coqc failed, signal an error or mark the job as \\+`failed', and
unlock ancestors as appropriate. If coqc was successful, trigger
-the transition 'enqueued-coqc -> 'ready for the job
+the transition \\+`enqueued-coqc' -> \\+`ready' for the job
behind PROCESS."
(let ((job (process-get process 'coq-compilation-job)))
(if (eq exit-status 0)
diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el
index 42f93c36b51..61cfad9c4f0 100644
--- a/coq/coq-seq-compile.el
+++ b/coq/coq-seq-compile.el
@@ -43,7 +43,7 @@
Lock only if `coq-lock-ancestor' is non-nil. Further, do nothing,
if ANCESTOR-SRC is already a member of
`proof-included-files-list'. Otherwise ANCESTOR-SRC is locked and
-registered in the 'coq-locked-ancestors property of the SPAN to
+registered in the \\+`coq-locked-ancestors' property of the SPAN to
properly unlock ANCESTOR-SRC on retract."
(if coq-lock-ancestors
(let ((true-ancestor-src (file-truename ancestor-src)))
@@ -150,14 +150,14 @@ if one of the following conditions is true:
Argument MAX-DEP-OBJ-TIME provides the information about the
dependencies. It is either
-- 'just-compiled if one of the dependencies of SRC has just
+- \\+`just-compiled' if one of the dependencies of SRC has just
been compiled
- the time value (see`time-less-or-equal') of the youngest (most
recently created) object file among the dependencies
- nil if there are no dependencies, or if they are all ignored
If this function decides to compile SRC to OBJ it returns
-'just-compiled. Otherwise it returns the modification time of
+\\+`just-compiled'. Otherwise it returns the modification time of
OBJ.
Note that file modification times inside Emacs have only a
@@ -189,7 +189,7 @@ OBJ have identical modification times."
"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
-not. This function returns 'just-compiled if it compiled
+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').
@@ -355,7 +355,7 @@ dependencies with \"coqdep\" and compiles modules as
necessary.
This internal checking does currently not handle ML modules.
Argument SPAN is the span of the \"Require\" command. Locked
-ancestors are registered in its 'coq-locked-ancestors property
+ancestors are registered in its \\+`coq-locked-ancestors' property
for proper unlocking on retract.
Argument COQ-OBJECT-LOCAL-HASH-SYMBOL provides a place to store
diff --git a/coq/coq-smie.el b/coq/coq-smie.el
index dbf032a6057..290f5937d22 100644
--- a/coq/coq-smie.el
+++ b/coq/coq-smie.el
@@ -87,7 +87,7 @@ indentation work well.
An example of configuration is:
- (setq coq-smie-user-tokens '((\"xor\" . \"or\") (\"ifb\" . \"if\")))
+ (setq coq-smie-user-tokens \\='((\"xor\" . \"or\") (\"ifb\" . \"if\")))
to have token \"xor\" and \"ifb\" be considered as having
respectively same priority and associativity as \"or\" and \"if\".
diff --git a/coq/coq-system.el b/coq/coq-system.el
index 933c1594b67..e9b3acd7f09 100644
--- a/coq/coq-system.el
+++ b/coq/coq-system.el
@@ -50,7 +50,7 @@
(defcustom coq-prog-env nil
"List of environment settings to pass to Coq process.
On Windows you might need something like:
- (setq coq-prog-env '(\"HOME=C:\\Program Files\\Coq\\\"))"
+ (setq coq-prog-env \\='(\"HOME=C:\\Program Files\\Coq\\\"))"
:group 'coq)
;; We just call "rocq" and look the error message that should mention
@@ -618,7 +618,7 @@ _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
and \"makefile generation\"):
@@ -630,14 +630,14 @@ 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
+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.
-alreadyopen is t if buffer already existed."
+ "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
(locate-dominating-file
@@ -692,7 +692,7 @@ Returns a mixed list of option-value pairs and strings."
OPTIONS is a list or conses (switch . argument) and strings.
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
diff --git a/coq/coq.el b/coq/coq.el
index 69967c170be..f9b25eae242 100644
--- a/coq/coq.el
+++ b/coq/coq.el
@@ -611,11 +611,11 @@ and read by function `coq-empty-action-list-command'.")
(span-set-property span 'statenum val))
(defsubst coq-get-span-goalcmd (span)
- "Return the 'goalcmd flag of the SPAN."
+ "Return the \\+`goalcmd' flag of the SPAN."
(span-property span 'goalcmd))
(defsubst coq-set-span-goalcmd (span val)
- "Set the 'goalcmd flag of the SPAN to VAL."
+ "Set the \\+`goalcmd' flag of the SPAN to VAL."
(span-set-property span 'goalcmd val))
(defsubst coq-set-span-proofnum (span val)
@@ -987,7 +987,7 @@ silent."
(defun coq-command-with-set-unset (setcmd cmd unsetcmd &optional postformatcmd
testcmd)
"Play commands SETCMD then CMD and then silently UNSETCMD.
-The last UNSETCMD is performed with tag 'empty-action-list so that it
+The last UNSETCMD is performed with tag \\+`empty-action-list' so that it
does not trigger `proof-shell-empty-action' (which does \"Show\" at
the time of writing this documentation). Also add
`'dont-show-when-silent' everywhere to suppress show commands when
@@ -1188,7 +1188,7 @@ With flag Printing All if some prefix arg is given
(\\[universal-argument])."
(coq-ask-do-show-all "Check" "Check"))
(defun coq-get-response-string-at (&optional pt)
- "Go forward from PT until reaching a 'response property, and return it.
+ "Go forward from PT until reaching a \\+`response' property, and return it.
Response span only starts at first non space character of a
command, so we may have to go forward to find it. Starts
from (point) if pt is nil. Precondition: pt (or point if nil)
@@ -2699,17 +2699,17 @@ Warning: this makes the error messages (and location)
wrong.")
Suggestions are emitted by Coq at Qed time. The possible values
of this variable are:
-- 'always: always insert the suggested annotation
+- \\+`always': always insert the suggested annotation
-- 'highlight (default value): highlight the Proof command and
+- \\+`highlight' (default value): highlight the Proof command and
have a contextual menu for insertion (or M-x
coq-insert-suggested-dependency when point is on the proof
considered)
-- 'ask: asks the user each time. If yes then do as 'always, else
- do as 'highlight
+- \\+`ask': asks the user each time. If yes then do as \\+`always', else
+ do as \\+`highlight'
-- 'never: ignore completely the suggestions.
+- \\+`never': ignore completely the suggestions.
Remarks and limitations:
- do not support nested proofs.
@@ -2718,7 +2718,7 @@ Remarks and limitations:
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
- generates an error. PG won't try to replace the erroneous
+ generates an error. PG will not 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 \\[coq-insert-suggested-dependency]
diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 2fefc0bf9d4..63c0b9df718 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -39,7 +39,7 @@
"Flag indicating overall successful state of tests.")
(defvar pg-autotest-log t
- "Value for 'standard-output' during tests.")
+ "Value for `standard-output' during tests.")
;;; Some utilities
@@ -117,7 +117,7 @@
(pg-autotest-message "\n\nREMARK: %s\n" msg))
(defun pg-autotest-timestart (&optional clockname)
- "Make a note of current time, named 'local or CLOCKNAME."
+ "Make a note of current time, named \\+`local' or CLOCKNAME."
(put 'pg-autotest-time (or clockname 'local)
(current-time)))
diff --git a/generic/pg-pamacs.el b/generic/pg-pamacs.el
index c603d1537fa..41ec5244cdc 100644
--- a/generic/pg-pamacs.el
+++ b/generic/pg-pamacs.el
@@ -47,7 +47,7 @@
(setq-default ,var ,value)))
(deflocal proof-buffer-type nil
- "Symbol for the type of this buffer: 'script, 'shell, 'goals, or 'response.")
+ "Symbol for the type of this buffer: \\+`script', \\+`shell', \\+`goals', or
\\+`response'.")
;;
@@ -238,8 +238,8 @@ which can be changed by sending commands.
In this case, NAME stands for the internal setting, flag, etc,
for the proof assistant, and a :setting and :type value should be
-provided. The :type of NAME should be one of 'integer, 'float,
-'boolean, 'string. Other types are not supported (see
+provided. The :type of NAME should be one of \\+`integer', \\+`float',
+\\+`boolean', \\+`string'. Other types are not supported (see
`proof-menu-entry-for-setting'). They will yield an error when
constructing the proof assistant menu.
diff --git a/generic/pg-response.el b/generic/pg-response.el
index 8e94439bd20..e11db9e2fac 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -131,7 +131,7 @@ Internal variable, setting this will have no effect!")
(defun proof-guess-3win-display-policy (&optional policy)
"Return the 3 windows mode layout policy from user choice POLICY.
-If POLICY is 'smart then guess the good policy from the current
+If POLICY is \\+`smart' then guess the good policy from the current
frame geometry, otherwise follow POLICY.
See `proof-layout-windows' for more details about POLICY."
@@ -144,7 +144,7 @@ See `proof-layout-windows' for more details about POLICY."
(defun proof-select-three-b (b1 b2 b3 &optional policy)
"Put the three buffers B1, B2, and B3 into three windows.
-Following POLICY, which can be 'smart, 'horizontal, 'vertical, or 'hybrid.
+Following POLICY, which can be \\+`smart', \\+`horizontal', \\+`vertical', or
\\+`hybrid'.
See `proof-layout-windows' for more details about POLICY.
@@ -249,7 +249,7 @@ dragging the separating bars.
- horizontal: 3 columns mode, one for each buffer (script, goals,
response).
- By default, the display mode is 'smart which automatically chooses
+ By default, the display mode is \\+`smart' which automatically chooses
between these 3 modes by considering the current Emacs frame width: if
it is smaller than `split-width-threshold' then vertical mode is
chosen, otherwise if it is smaller than 1.5 * `split-width-threshold'
@@ -260,8 +260,8 @@ dragging the separating bars.
will.
If you want to force one of the layouts, you can set variable
- `proof-three-window-mode-policy' to 'vertical, 'horizontal or
- 'hybrid. The default value is 'smart which sets the automatic
+ `proof-three-window-mode-policy' to \\+`vertical', \\+`horizontal' or
+ \\+`hybrid'. The default value is \\+`smart' which sets the automatic
behaviour described above."
(interactive)
(cond
@@ -340,7 +340,7 @@ dragging the separating bars.
Mainly, we look at `pg-response-erase-flag' and clear the
response buffer if this is non-nil, but NOT the special
-symbol 'invisible.
+symbol \\+`invisible'.
ERASE-NEXT-TIME is the new value for the flag.
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 8e490eb8e1d..312a40e2887 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -533,7 +533,7 @@ This is intended as a value for
`proof-activate-scripting-hook'"
;;;###autoload
(defun proof-electric-terminator-enable (&optional arg)
"Ensure modeline update to display new value for electric terminator.
-This a function is called by the custom-set property 'proof-set-value.
+This a function is called by the custom-set property \\+`proof-set-value'.
It can also be used as a minor mode function: with ARG, turn on iff ARG>0"
(unless (null arg)
(setq proof-electric-terminator-enable (> (prefix-numeric-value arg) 0)))
@@ -726,14 +726,14 @@ CHUNKS must be the reversed result of
`proof-script-omit-filter'
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.
+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
+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
of `proof-omit-cheating-regexp', if defined, count as failing,
@@ -742,12 +742,12 @@ proof-status result is a list of 4 elements as follows.
`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
+ \\+`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
- using\". More precisely, it is the last span in the 'no-proof
+ using\". More precisely, it is the last span in the \\+`no-proof'
chunk before the proof."
(let (proof-results current-proof-state-and-name proof-start-points)
(while chunks
@@ -886,7 +886,7 @@ invalid proof.
Argument TAP, which can be set by a prefix argument, controls the
form of the generated overview. Nil, without prefix, gives an
-human readable overview, otherwise it's test anything
+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
@@ -900,7 +900,7 @@ 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
Coq for instance, among others, proof scripts terminated with
-'Defined' are not opaque and do not appear in the generated
+\"Defined\" are not opaque and do not appear in the generated
overview.
Note that this command does not (re-)compile required files.
@@ -1674,7 +1674,7 @@ Assume the `undo-in-region' behavior will apply if ARG is
non-nil."
(defvar proof-autosend-timer nil "Timer used by autosend.")
(deflocal proof-autosend-modified-tick nil
- "Records 'buffer-chars-modified-tick' since last autosend.")
+ "Records `buffer-chars-modified-tick' since last autosend.")
;;;###autoload
(defun proof-autosend-enable (&optional nomsg)
diff --git a/generic/pg-vars.el b/generic/pg-vars.el
index 49ca5c945c9..44977b3eb4c 100644
--- a/generic/pg-vars.el
+++ b/generic/pg-vars.el
@@ -96,7 +96,7 @@ to script management from a buffer (rather than being ad-hoc
query commands to the prover).
When processing commands from a buffer for script management,
-this will be set to the queue mode 'advancing or 'retracting to
+this will be set to the queue mode \\+`advancing' or \\+`retracting' to
indicate the direction of movement.
When this is non-nil, `proof-shell-ready-prover' will give
@@ -157,7 +157,7 @@ See `proof-shell-thm-display-regexp' for details.")
(defvar proof-shell-error-or-interrupt-seen nil
"Flag indicating that an error or interrupt has just occurred.
-Set to 'error or 'interrupt if one was observed from the proof
+Set to \\+`error' or \\+`interrupt' if one was observed from the proof
assistant during the last group of commands.")
(defvar pg-response-next-error nil
@@ -192,12 +192,12 @@ This is raw string, for internal use only.")
"A symbol denoting the type of the last output string from the proof system.
Specifically:
- 'interrupt An interrupt message
- 'error An error message
- 'loopback A command sent from the PA to be inserted into the script
- 'response A response message
- 'goals A goals (proof state) display
- 'systemspecific Something specific to a particular system,
+ \\+`interrupt' An interrupt message
+ \\+`error' An error message
+ \\+`loopback' A command sent from the PA to be inserted into the script
+ \\+`response' A response message
+ \\+`goals' A goals (proof state) display
+ \\+`systemspecific' Something specific to a particular system,
-- see `proof-shell-handle-output-system-specific'
The output corresponding to this will be in `proof-shell-last-output'.
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 6239426f0a4..89543269840 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -325,8 +325,8 @@ point the position where the parse should begin. It should
move point to the exact end of the next \"segment\", and return
a symbol indicating what has been parsed:
- 'comment for a comment
- 'cmd for a proof script command
+ \\+`comment' for a comment
+ \\+`cmd' for a proof script command
nil if there is no complete next segment in the buffer
If this is left unset, it will be configured automatically to
@@ -471,11 +471,11 @@ may be left as nil."
Used for provers which allow nested atomic goal-saves, but with some
nested history that must be undone specially.
-At the moment, the behaviour is that a goal-save span has a 'nestedundos
+At the moment, the behaviour is that a goal-save span has a \\+`nestedundos'
property which is set to the number of commands within it which match
this regexp. The idea is that the prover-specific code can create a
customized undo command to retract the goal-save region, based on the
-'nestedundos setting. Coq uses this to forget declarations, since
+\\+`nestedundos' setting. Coq uses this to forget declarations, since
declarations in Coq reside in a separate context with its own (flat)
history."
:type '(choice (const nil) regexp)
@@ -529,14 +529,14 @@ off the goal..[save] region in more flexible ways.
The possibilities are:
nil - nothing special; close only when a save arrives
- 'closeany - close as soon as the next command arrives, save or not
- 'closegoal - close when the next \"goal\" command arrives
- 'extend - keep extending the closed region until a save or goal.
+ \\+`closeany' - close as soon as the next command arrives, save or not
+ \\+`closegoal' - close when the next \"goal\" command arrives
+ \\+`extend' - keep extending the closed region until a save or goal.
If your proof assistant allows nested goals, it will be wrong to close
off the portion of proof so far, so this variable should be set to nil.
-NB: 'extend behaviour is not currently compatible with appearance of
+NB: \\+`extend' behaviour is not currently compatible with appearance of
save commands, so don't use that if your prover has save commands."
:type '(choice
(const :tag "Close on save only" nil)
@@ -588,7 +588,7 @@ you only need to set if you use that function (by not
customizing
"Function to return cons if point is at a goal/hypothesis/literal.
This is used to parse the proofstate output to mark it up for
proof-by-pointing or literal command insertion. It should return a cons or
nil.
-First element of the cons is a symbol, 'goal', 'hyp' or 'lit'.
+First element of the cons is a symbol, \\+`goal', \\+`hyp' or \\+`lit'.
The second element is a string: the goal, hypothesis, or literal command
itself.
If you leave this variable unset, no proof-by-pointing markup
@@ -639,7 +639,7 @@ The classic behaviour of Proof General is to undo completed
proofs in one step: this design arose because older provers
discarded nested history once proofs were complete. The proof
script engine amalgamates spans for a complete proof (into a
-single 'goalsave) to give this effect.
+single \\+`goalsave') to give this effect.
Newer designs keep more state, and may support arbitrary undo
with a file being processed. If this flag is non-nil,
@@ -853,7 +853,7 @@ the proof assistant back to the same state."
:group 'proof-script)
(defcustom proof-indent-hang nil
- "Enable 'hanging' indentation for proof script."
+ "Enable hanging indentation for proof script."
:type 'boolean
:group 'proof-script)
@@ -1673,7 +1673,7 @@ by the cdr.
For example, when directories are sent to Isabelle, HOL, and Coq,
they appear inside ML strings and the backslash character and
quote characters must be escaped. The setting
- '((\"\\\\\\\\\" . \"\\\\\\\\\")
+ \\='((\"\\\\\\\\\" . \"\\\\\\\\\")
(\"\\\"\" . \"\\\\\\\"\"))
achieves this.
@@ -1738,12 +1738,12 @@ shell filter once `string' has been processed. The
`action' variable
suggests what class of command is about to be inserted, the first two
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 suppressed
- 'proof-shell-clear-silent Indicates prover output has been restored
- 'init-cmd Early initialization command sent to prover
+ \\+`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 suppressed
+ \\+`proof-shell-clear-silent' Indicates prover output has been restored
+ \\+`init-cmd' Early initialization command sent to prover
Caveats: You should be very careful about setting this hook. Proof
General relies on a careful synchronization with the process between
@@ -1867,7 +1867,7 @@ be prevented, the function should update the variable
The symbol will be compared against standard ones, see documentation
of `proof-shell-last-output-kind'. A suggested canonical non-standard
-symbol is 'systemspecific."
+symbol is \\+`systemspecific'."
:type '(repeat function)
:group 'proof-shell)
diff --git a/generic/proof-script.el b/generic/proof-script.el
index 133a4f13230..b7d456e84b6 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -381,7 +381,7 @@ value of proof-locked span."
"Remove the queue span from buffer, cleaning spans no longer queued.
If BADSPAN is non-nil, assume that this was the span whose command
caused the error. Go to the start of it if `proof-follow-mode' is
-'locked.
+\\+`locked'.
If INTERRUPTP is non-nil, do not consider BADSPAN itself as faulty.
@@ -404,14 +404,14 @@ This is a subroutine used in
proof-shell-handle-{error,interrupt}."
(proof-script-delete-spans start end)))
(defun proof-script-delete-spans (beg end)
- "Delete primary spans between BEG and END. Secondary 'pghelp spans are
left."
+ "Delete primary spans between BEG and END. Secondary \\+`pghelp' spans are
left."
(span-delete-spans beg end 'type)
(span-delete-spans beg end 'idiom)
(span-delete-spans beg end 'pg-span)
)
(defun proof-script-delete-secondary-spans (beg end)
- "Delete secondary spans between BEG and END (currently, 'pghelp spans)."
+ "Delete secondary spans between BEG and END (currently, \\+`pghelp' spans)."
(span-delete-spans beg end 'pghelp))
@@ -515,7 +515,7 @@ If called interactively, a mark is set at the current
location with `push-mark'"
"If the end of the locked region is not visible, jump to the end of it.
A possible hook function for `proof-shell-handle-error-or-interrupt-hook'.
Does nothing if there is no active scripting buffer, or if
-`proof-follow-mode' is set to 'ignore."
+`proof-follow-mode' is set to \\+`ignore'."
(interactive)
(if (and proof-script-buffer
(not (eq proof-follow-mode 'ignore)))
@@ -595,7 +595,7 @@ will be recorded as a textual name used instead of ID for
users;
NAME does not need to be unique.
NAME is a name that comes from the proof script or prover output.
-It is recorded in the span with the 'rawname property."
+It is recorded in the span with the \\+`rawname' property."
(cl-assert (symbolp idiomsym))
(cl-assert (stringp id))
(if name (cl-assert (stringp name)))
@@ -633,12 +633,12 @@ It is recorded in the span with the 'rawname property."
(defun pg-invisible-prop (idiom)
"Return an invisibility symbol for the given IDIOM.
-This is a value for the overlay 'invisible property."
+This is a value for the overlay \\+`invisible' property."
(intern (concat "pg-" (symbol-name (or idiom 'other)))))
(defun pg-set-element-span-invisible (span invisiblep)
"Function to adjust visibility of SPAN to INVISIBLEP.
-We use list values of the 'invisible property which contain
+We use list values of the \\+`invisible' property which contain
private symbols, that should play well with other conforming modes
and `buffer-invisibility-spec'."
(let* ((invisible-prop (pg-invisible-prop (span-property span 'idiom)))
@@ -712,13 +712,13 @@ IDIOMSYM is a symbol and ID is a strings."
"Return a user-level name for SPAN.
This is based on its name and type.
-Each span has a 'type property, one of:
+Each span has a \\+`type' property, one of:
- 'goalsave A goal..savegoal region in the buffer, a completed proof.
- '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."
+ \\+`goalsave' A goal..savegoal region in the buffer, a completed proof.
+ \\+`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."
(let ((type (span-property span 'type))
(idiom (span-property span 'idiom))
(rawname (span-property span 'rawname)))
@@ -773,7 +773,7 @@ This is used to annotate the buffer with the result of
proof steps."
The daughter span covers the non whitespace content of the main span.
We add the last output (when non-empty) to the hover display, and
-also as the 'response property on the span.
+also as the \\+`response' property on the span.
Optional argument MOUSEFACE means use the given face as a mouse highlight
face, if it is a face, otherwise, if it is non-nil but not a face,
@@ -782,7 +782,7 @@ do not add a mouse highlight.
In any case, a mouse highlight and tooltip are only set if
`proof-output-tooltips' is non-nil.
-Argument FACE means add 'face property FACE to the span."
+Argument FACE means add \\+`face' property FACE to the span."
(let* ((output (pg-last-output-displayform))
(new-start (save-excursion
(goto-char (span-start span))
@@ -1077,7 +1077,7 @@ Otherwise retract it. Errors are ignored"
(defun proof-deactivate-scripting-query-user-action ()
"Display the script and query the user for a deactivate action.
-Returns 'retract, 'process or finally nil if user declined."
+Returns \\+`retract', \\+`process' or finally nil if user declined."
;; Would be nicer to ask a single question, but
;; a nuisance to define our own dialogue since it
;; doesn't really fit with one of the standard ones.
@@ -1120,7 +1120,7 @@ Returns 'retract, 'process or finally nil if user
declined."
nil)))))
(defun proof-deactivate-scripting-choose-action ()
- "Select a deactivation action, 'process, 'retract or nil."
+ "Select a deactivation action, \\+`process', \\+`retract' or nil."
(let ((auto-action
(if (and proof-no-fully-processed-buffer
(eq proof-auto-action-when-deactivating-scripting
@@ -1147,7 +1147,7 @@ user option
`proof-auto-action-when-deactivating-scripting'.
If `proof-no-fully-processed-buffer' is t there is only the choice
to fully retract the active scripting buffer. In this case the
active scripting buffer is retracted even if it was fully processed.
-Setting `proof-auto-action-when-deactivating-scripting' to 'process
+Setting `proof-auto-action-when-deactivating-scripting' to \\+`process'
is ignored in this case.
If the scripting buffer is (or has become) fully processed, and it is
@@ -1379,9 +1379,9 @@ Argument SPAN has just been processed.
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,
+- creates additional spans (without \\+`type' property) for help,
tooltips, color and menus
-- merges spans with 'type as needed to achieve atomic undo for
+- merges spans with \\+`type' as needed to achieve atomic undo for
proofs and sections
- enters some commands and their spans in some database (with for
me unknown purpose)"
@@ -1478,10 +1478,10 @@ that is not yet documented here, this function
"Retire commands that close a proof or some other region.
This is a subroutine of `proof-done-advancing'.
Besides stuff that is not yet documented here, this function
-- creates additional spans (without 'type property) for help,
+- creates additional spans (without \\+`type' property) for help,
tooltips, color and menus
- in particular, adds the background color for omitted proofs
-- merges spans with 'type as needed to achieve atomic undo for
+- merges spans with \\+`type' as needed to achieve atomic undo for
proofs and sections; for Coq this is done at least for proofs
and sections.
- enters some commands and their spans in some database (with for
@@ -1737,7 +1737,7 @@ them by type. Return a list of lists of the form
where:
- TYPE is a symbol indicating the type of text found, either 'cmd or 'comment;
+ TYPE is a symbol indicating the type of text found, either \\+`cmd' or
\\+`comment';
TEXT is the string content taken from the buffer;
ENDPOS is the position of the final character of the text.
@@ -2031,14 +2031,14 @@ 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
+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
-adjacent 'no-proof chunks, for instance for commands outside a
+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:
+The \\+`proof' chunk has 4 elements:
\('proof proof-cmds-reversed span-start-first-proof-cmd
span-end-first-proof-cmd)
@@ -2052,21 +2052,21 @@ start of the command that matched
`proof-script-proof-start-regexp' and span-end-first-proof-cmd is
the position of the end of that command.
-The 'no-proof chunk has 2 elements.
+The \\+`no-proof' chunk has 2 elements.
\('no-proof cmds-reversed)
cmds-reversed contains the vanilla spans of VANILLAS in reversed
order.
-The 'nested-proof chunk has 3 elements.
+The \\+`nested-proof' chunk has 3 elements.
\('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
-there is a 'nested-proof chunk in the result, it is the first
+there is a \\+`nested-proof' chunk in the result, it is the first
chunk."
(cl-assert
(and proof-omit-proofs-configured proof-script-proof-start-regexp
@@ -2199,7 +2199,7 @@ opaque proofs in the action list VANILLAS. Additionally,
it uses
`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
-contains an 'omitted-proof-region property with the region of the
+contains an \\+`omitted-proof-region' property with the region of the
omitted proof. This is used in `proof-done-advancing-save' to
colour the omitted proof with `proof-omitted-proof-face'.
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 3746662c62c..960b61728e1 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -103,7 +103,7 @@ prover. It might be the empty list if nothing needs to be
sent to
the prover, such as, for comments. Usually COMMANDS
contains just 1 string, but it might also contains more elements.
The text should be obtained with
-`(mapconcat 'identity COMMANDS \" \")', where the last argument
+`(mapconcat \\='identity COMMANDS \" \")', where the last argument
is a space.
ACTION is the callback to be invoked when this item has been
@@ -117,24 +117,24 @@ The DISPLAYFLAGS are set
for non-scripting commands or for when scripting should not
bother the user. They may include
- 'invisible non-script command (`proof-shell-invisible-command')
- 'no-response-display do not display messages in *response* buffer
- 'no-error-display do not display errors/take error action
- 'no-goals-display do not goals in *goals* buffer
- 'keep-response do not erase the response buffer when goals are
shown
- 'proof-tree-show-subgoal item inserted by the proof-tree package to display
+ \\+`invisible' non-script command
(`proof-shell-invisible-command')
+ \\+`no-response-display' do not display messages in *response* buffer
+ \\+`no-error-display' do not display errors/take error action
+ \\+`no-goals-display' do not goals in *goals* buffer
+ \\+`keep-response' do not erase the response buffer when goals
are shown
+ \\+`proof-tree-show-subgoal' item inserted by the proof-tree package to
display
the current or some other goal
- 'proof-tree-last-item marks the item that follows the last show-goal
+ \\+`proof-tree-last-item' marks the item that follows the last show-goal
request after a proof finished with proof-tree
display, causes switch back to normal queue region
processing
- 'priority-action item added via proof-add-to-priority-queue
- 'empty-action-list proof-shell-empty-action-list-command should not be
+ \\+`priority-action' item added via proof-add-to-priority-queue
+ \\+`empty-action-list' proof-shell-empty-action-list-command should
not be
called if this is the last item in the action list
- 'dont-show-when-silent Used for commands that should not be followed by a
+ \\+`dont-show-when-silent' Used for commands that should not be followed
by a
show command when running silent.
-Note that 'invisible does not imply any of the others. If flags
+Note that \\+`invisible' does not imply any of the others. If flags
are non-empty, interactive cues will be suppressed. (E.g.,
printing hints).
@@ -764,7 +764,7 @@ This is a subroutine of `proof-shell-handle-error'."
(defun proof-shell-handle-error-or-interrupt (err-or-int flags)
"React on an error or interrupt message triggered by the prover.
-The argument ERR-OR-INT should be set to 'error or 'interrupt
+The argument ERR-OR-INT should be set to \\+`error' or \\+`interrupt'
which affects the action taken.
For errors, we first flush unprocessed output (usually goals).
@@ -776,12 +776,12 @@ In both cases we then sound a beep, clear the queue and
spans and
finally we call `proof-shell-handle-error-or-interrupt-hook'.
Commands which are not part of regular script management (with
-FLAGS containing 'no-error-display) will not cause any display action.
+FLAGS containing \\+`no-error-display') will not cause any display action.
This is called in two places: (1) from the output processing
functions, in case we find an error or interrupt message output,
and (2) from the exec loop, in case of a pending interrupt which
-didn't cause prover output."
+didn\\='t cause prover output."
(unless (memq 'no-error-display flags)
(cond
((eq err-or-int 'interrupt)
@@ -812,7 +812,7 @@ didn't cause prover output."
(defun proof-shell-error-or-interrupt-action (err-or-int)
"Take action on errors or interrupts.
-ERR-OR-INT is a flag, 'error or 'interrupt.
+ERR-OR-INT is a flag, \\+`error' or \\+`interrupt'.
This is a subroutine of `proof-shell-handle-error-or-interrupt'.
Must be called with proof shell buffer current.
@@ -1187,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)
@@ -1213,7 +1213,7 @@ This function calls `proof-add-to-queue' with args
QUEUEITEMS and QUEUEMODE."
"Extend the current queue with QUEUEITEMS, queue end END.
To make sense, the commands should correspond to processing actions
for processing a region from (buffer-queue-or-locked-end) to END.
-The queue mode is set to 'advancing"
+The queue mode is set to \\+`advancing'"
(proof-set-queue-endpoints (proof-unprocessed-begin) end)
(condition-case err
(run-hooks 'proof-shell-extend-queue-hook)
@@ -1794,7 +1794,7 @@ by the filter is to send the next command from the queue."
"Display delayed goals/responses, when queue is stopped or completed.
This function handles the cases of `proof-shell-output-kind' which
are not dealt with eagerly during script processing, namely
-'response and 'goals types.
+\\+`response' and \\+`goals' types.
This is useful even with empty delayed output as it will empty
the buffers.
@@ -1835,7 +1835,7 @@ The goals and response outputs are copied into
`proof-shell-last-response-output' respectively.
The value returned is the value for `proof-shell-last-output-kind',
-i.e., 'goals or 'response."
+i.e., \\+`goals' or \\+`response'."
(let ((start proof-shell-delayed-output-start)
(end proof-shell-delayed-output-end)
(flags proof-shell-delayed-output-flags))
@@ -2029,7 +2029,7 @@ if it is set. It should probably run the hook variables
`proof-state-change-hook'.
FLAGS are additional flags to put onto the `proof-action-list'.
-The flag 'invisible is always added to FLAGS."
+The flag \\+`invisible' is always added to FLAGS."
(unless (stringp cmd)
(setq cmd (eval cmd)))
(if cmd
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index dc2ff0bc9f9..c01eb1bfba1 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -148,7 +148,7 @@ The returned value is one of the following symbols:
(defun proof-looking-at-syntactic-context ()
"Determine if current point is at beginning or within comment/string context.
-If so, return a symbol indicating this ('comment or 'string).
+If so, return a symbol indicating this (\\+`comment' or \\+`string').
This function invokes <PA-syntactic-context> if that is defined, otherwise
it calls `proof-looking-at-syntactic-context'."
(if (fboundp (proof-ass-sym syntactic-context))
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index b19cf31629a..1b0500f64c7 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -345,7 +345,7 @@ An action item is a list `(SPAN COMMANDS ACTION
[DISPLAYFLAGS])',
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
-will add 'proof-tree-last-item to DISPLAYFLAGS when necessary."
+will add \\+`proof-tree-last-item' to DISPLAYFLAGS when necessary."
:type 'function
:group 'proof-tree-internals)
@@ -557,7 +557,7 @@ This function is called in 4 situations.
(defun proof-tree-confirm-proof-complete (data)
"Callback function for confirm-proof-complete messages.
Add command `proof-tree-display-stop-command' with
-'proof-tree-last-item flag, such that
+\\+`proof-tree-last-item' flag, such that
`proof-tree-check-proof-finish' eventually sees this last command
and switches the proof-tree display processing off."
(if (string-match proof-tree--confirm-complete-regexp data)
@@ -1103,7 +1103,7 @@ goal command. OLD-PROOF-INFO must be the result of
This function processes delayed output that the proof assistant
generated in response to commands that prooftree inserted in
order to keep its display up-to-date. Such commands are tagged
-with a 'proof-tree-show-subgoal flag. Argument PROOF-NAME
+with a \\+`proof-tree-show-subgoal' flag. Argument PROOF-NAME
originally comes from prooftree and is passed back now, because
processing a show goal command might happen after the proof.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index be8634b49cb..519eabf0add 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -178,7 +178,7 @@ done if this `proof-strict-state-preserving' is turned off
(nil)."
(defcustom proof-strict-read-only 'retract
"*Whether Proof General is strict about the read-only region in buffers.
If non-nil, an error is given when an attempt is made to edit the
-read-only region, except for the special value 'retract which means
+read-only region, except for the special value \\+`retract' which means
undo first. If nil, Proof General is more relaxed (but may give
you a reprimand!)."
:type '(choice
@@ -232,11 +232,11 @@ and displayed lazily. See `proof-layout-windows'."
(defcustom proof-three-window-mode-policy 'smart
"*Window splitting policy for three window mode.
-- If 'vertical forces one column mode.
-- If 'horizontal forces 3 column mode
-- If 'hybrid forces 2 columns mode
-- If 'smart or anything else: 'horizontal when the window is wide
- enough, then hybrid if wide enough and 'vertical otherwise. The width
+- If \\+`vertical' forces one column mode.
+- If \\+`horizontal' forces 3 column mode
+- If \\+`hybrid' forces 2 columns mode
+- If \\+`smart' or anything else: \\+`horizontal' when the window is wide
+ enough, then hybrid if wide enough and \\+`vertical' otherwise. The width
threshold is given by `split-width-threshold'.
See `proof-layout-windows'."
@@ -253,7 +253,7 @@ and displayed lazily. See `proof-layout-windows'."
For example, at the end of a proof the goals buffer window will
be cleared; if this flag is set it will automatically be removed.
If you want to fix the sizes of your windows you may want to set this
-variable to 'nil' to avoid windows being deleted automatically.
+variable to nil to avoid windows being deleted automatically.
If you use multiple frames, only the windows in the currently
selected frame will be automatically deleted."
:type 'boolean
@@ -376,14 +376,14 @@ This variable exists to disable the cache in case of
problems."
(defcustom proof-follow-mode 'locked
"*Choice of how point moves with script processing commands.
-One of the symbols: 'locked, 'follow, 'followdown, 'ignore.
+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 writable region
-If 'ignore, point is never moved after movement commands or on errors.
+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 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
+If you choose \\+`ignore', you can find the end of the locked using
\\[proof-goto-end-of-locked]"
:type '(choice
(const :tag "Follow locked region" locked)
@@ -399,9 +399,9 @@ If you choose 'ignore, you can find the end of the locked
using
;; ancestor file). And in that case (supposing file being unlocked is
;; an ancestor), it seems unlikely that we need to query for saves.
(defcustom proof-auto-action-when-deactivating-scripting nil
- "*If 'retract or 'process, do that when deactivating scripting.
+ "*If \\+`retract' or \\+`process', do that when deactivating scripting.
-With this option set to 'retract or 'process, when scripting
+With this option set to \\+`retract' or \\+`process', when scripting
is turned off in a partly processed buffer, the buffer will be
retracted or processed automatically.
@@ -417,7 +417,7 @@ locked (coloured blue); a buffer is completely unprocessed
when there
is no locked region.
For some proof assistants (such as Coq) fully processed buffers make
-no sense. Setting this option to 'process has then the same effect
+no sense. Setting this option to \\+`process' has then the same effect
as leaving it unset (nil). (This behaviour is controlled by
`proof-no-fully-processed-buffer'.)"
:type '(choice
diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el
index 247250651b4..d2b5ec8dc68 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
diff --git a/lib/span.el b/lib/span.el
index 08e4bb2cdbd..d9eb9f345db 100644
--- a/lib/span.el
+++ b/lib/span.el
@@ -89,7 +89,7 @@
(car-safe (spans-at-point-prop pt prop)))
(defun span-delete (span)
- "Run the 'span-delete-actions and delete SPAN."
+ "Run the \\+`span-delete-actions' and delete SPAN."
(mapc #'funcall (span-property span 'span-delete-actions))
(delete-overlay span))
@@ -165,7 +165,7 @@ A span is before PT if it begins before the character
before PT."
(setq plist (cddr plist))))
(defun span-at-event (event &optional prop)
- "Find a span at position of EVENT, with property PROP (default 'span)."
+ "Find a span at position of EVENT, with property PROP (default \\+`span')."
(car (spans-filter
(overlays-at (posn-point (event-start event)))
(or prop 'span))))
diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el
index 52a1869f5c2..4ec0dd69753 100644
--- a/lib/unicode-tokens.el
+++ b/lib/unicode-tokens.el
@@ -590,7 +590,7 @@ Optional argument OBJECT is the string or buffer containing
the text."
(defun unicode-tokens-symbs-to-props (symbs &optional facenil)
"Turn the property name list SYMBS into a list of text properties.
Symbols are looked up in `unicode-tokens-fontsymb-properties'.
-Optional argument FACENIL means set the face property to nil, unless 'face is
in the property list."
+Optional argument FACENIL means set the face property to nil, unless \\+`face'
is in the property list."
(let (props ps)
(dolist (s symbs)
(setq ps (cdr-safe
