branch: elpa/proof-general
commit ccf90d6baefe80bcd0c0d7d86573471cad5bec49
Author: Morgan Smith <[email protected]>
Commit: Morgan Smith <[email protected]>
Quote symbol-names in docstring correctly
---
generic/pg-user.el | 8 ++++----
generic/proof-config.el | 8 ++++----
generic/proof-shell.el | 2 +-
generic/proof-tree.el | 8 ++++----
generic/proof-useropts.el | 2 +-
generic/proof-utils.el | 6 +++---
6 files changed, 17 insertions(+), 17 deletions(-)
diff --git a/generic/pg-user.el b/generic/pg-user.el
index 312a40e2887..92078f085c6 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -411,8 +411,8 @@ a proof command."
BODY defaults to CMDVAR, a variable."
`(defun ,fn ()
,(concat doc
- (concat "\nIssues a command to the assistant based on "
- (symbol-name cmdvar) ".")
+ (concat "\nIssues a command to the assistant based on `"
+ (symbol-name cmdvar) "'.")
"")
(interactive)
(proof-if-setting-configured ,cmdvar
@@ -427,8 +427,8 @@ CMDVAR is a variable holding a function or string.
Automatically has history."
(defvar ,(intern (concat (symbol-name fn) "-history")) nil
,(concat "History of arguments for " (symbol-name fn) "."))
(defun ,fn (arg)
- ,(concat doc "\nIssues a command based on ARG to the assistant, using "
- (symbol-name cmdvar) ".\n"
+ ,(concat doc "\nIssues a command based on ARG to the assistant, using `"
+ (symbol-name cmdvar) "'.\n"
"The user is prompted for an argument.")
(interactive
(proof-if-setting-configured ,cmdvar
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 89543269840..9ebf7bfd092 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -562,7 +562,7 @@ settings `proof-non-undoables-regexp' and
This setting is used to for retraction (undoing) in proof scripts.
It should undo the effect of all settings between its target span
-up to (proof-unprocessed-begin). This may involve forgetting a number
+up to `proof-unprocessed-begin'. This may involve forgetting a number
of definitions, declarations, or whatever.
If return value is nil, it means there is nothing to do.
@@ -1039,8 +1039,8 @@ the escape sequences in `proof-shell-filename-escapes' are
applied to the filename.
This setting is used to define the function `proof-cd' which
-changes to the value of (default-directory) for script buffers.
-For files, the value of (default-directory) is simply the
+changes to the value of `default-directory' for script buffers.
+For files, the value of `default-directory' is simply the
directory the file resides in.
NB: By default, `proof-cd' is called from `proof-activate-scripting-hook',
@@ -2064,7 +2064,7 @@ and `proof-response-font-lock-keywords'."
(defcustom pg-before-fontify-output-hook nil
"This hook is called before fontifying a region in an output buffer.
A function on this hook can alter the region of the buffer within
-the current restriction, and must return the final value of (point-max).
+the current restriction, and must return the final value of `point-max'.
\[This hook is presently only used by phox-sym-lock]."
:type '(repeat function)
:group 'proof-goals)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 960b61728e1..cf8a2abce81 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -1800,7 +1800,7 @@ This is useful even with empty delayed output as it will
empty
the buffers.
The delayed output is in the region
-\[proof-shell-delayed-output-start,proof-shell-delayed-output-end].
+\[`proof-shell-delayed-output-start', `proof-shell-delayed-output-end'].
If no goals classified output is found, the whole output is
displayed in the response buffer.
diff --git a/generic/proof-tree.el b/generic/proof-tree.el
index 1b0500f64c7..33b59d64e16 100644
--- a/generic/proof-tree.el
+++ b/generic/proof-tree.el
@@ -992,7 +992,7 @@ without input from this function, whether or not a new
layer in
the proof tree must be started.
The delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
+\[`proof-shell-delayed-output-start', `proof-shell-delayed-output-end'].
Urgent messages might be before that, following OLD-PROOF-MARKER,
which contains the position of `proof-marker', before the next
command was sent to the proof assistant."
@@ -1037,7 +1037,7 @@ This function is called if there was a navigation
command, which
results in a different goal being current now.
The delayed output of the navigation command is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+\[`proof-shell-delayed-output-start', `proof-shell-delayed-output-end']."
(let ((start proof-shell-delayed-output-start)
(end proof-shell-delayed-output-end)
(proof-state (car proof-info))
@@ -1113,7 +1113,7 @@ output. If something is found an appropriate
update-sequent
command is sent to prooftree.
The delayed output is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end]."
+\[`proof-shell-delayed-output-start', `proof-shell-delayed-output-end']."
;; (message "PTUS buf %s output %d-%d state %s"
;; (current-buffer)
;; proof-shell-delayed-output-start proof-shell-delayed-output-end
@@ -1140,7 +1140,7 @@ delayed output in order to take appropriate actions and
maintains the
internal state.
The delayed output to handle is in the region
-\[proof-shell-delayed-output-start, proof-shell-delayed-output-end].
+\[`proof-shell-delayed-output-start', `proof-shell-delayed-output-end'].
Urgent messages might be before that, following OLD-PROOF-MARKER,
which contains the position of `proof-marker', before the next
command was sent to the proof assistant.
diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el
index 519eabf0add..bba559d62c9 100644
--- a/generic/proof-useropts.el
+++ b/generic/proof-useropts.el
@@ -42,7 +42,7 @@ setting.
If there is no function SYM, we try stripping
`proof-assistant-symbol' and adding \"proof-\" instead to get
-a function name. This extends proof-set-value to work with
+a function name. This extends `proof-set-value' to work with
generic individual settings.
The dynamic action call only happens when values *change*: as an
diff --git a/generic/proof-utils.el b/generic/proof-utils.el
index e5e8e538ff3..1789d0bf84f 100644
--- a/generic/proof-utils.el
+++ b/generic/proof-utils.el
@@ -540,7 +540,7 @@ Args as for the macro `proof-deftoggle', except will be
evaluated."
`(defun ,(if othername othername
(intern (concat (symbol-name var) "-toggle"))) (&optional arg)
,(concat "Toggle `" (symbol-name var) "'. With ARG, turn on iff
ARG>0.
-This function simply uses customize-set-variable to set the variable.")
+This function simply uses `customize-set-variable' to set the variable.")
; It was constructed with `proof-deftoggle-fn'."
(interactive "P")
(customize-set-variable
@@ -566,7 +566,7 @@ Args as for the macro `proof-defintset', except will be
evaluated."
`(defun ,(if othername othername
(intern (concat (symbol-name var) "-intset"))) (arg)
,(concat "Set `" (symbol-name var) "' to ARG.
-This function simply uses customize-set-variable to set the variable.
+This function simply uses `customize-set-variable' to set the variable.
It was constructed with `proof-defintset-fn'.")
(interactive (list
(read-number
@@ -592,7 +592,7 @@ Args as for the macro `proof-deffloatset', except will be
evaluated."
`(defun ,(if othername othername
(intern (concat (symbol-name var) "-floatset"))) (arg)
,(concat "Set `" (symbol-name var) "' to ARG.
-This function simply uses customize-set-variable to set the variable.
+This function simply uses `customize-set-variable' to set the variable.
It was constructed with `proof-deffloatset-fn'.")
(interactive (list
(read-number
