diff --git a/ci/compile-tests/007-slow-require/runtest.el b/ci/compile-tests/007-slow-require/runtest.el index 9d7ee38bf..e2f7b7a6a 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 18d9777f0..f249263fa 100644 --- a/ci/compile-tests/cct-lib.el +++ b/ci/compile-tests/cct-lib.el @@ -42,10 +42,10 @@ "Set to t to get more output during test runs.") (defvar cct-before-busy-waiting-hook nil - "Hooks run by ‘cct-process-to-line’ before busy waiting.") + "Hooks run by `cct-process-to-line' before busy waiting.") (defvar cct-after-busy-waiting-hook nil - "Hooks run by ‘cct-process-to-line’ after busy waiting.") + "Hooks run by `cct-process-to-line' after busy waiting.") (defmacro cct-implies (p q) @@ -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-compile-common.el b/coq/coq-compile-common.el index b07ac1b91..c85db0c1f 100644 --- a/coq/coq-compile-common.el +++ b/coq/coq-compile-common.el @@ -78,7 +78,7 @@ Must be used together with `coq-par-enable'." (defun coq-switch-compilation-method () - "Set function for function ‘coq-compile-parallel-in-background’." + "Set function for function `coq-compile-parallel-in-background'." (if coq-compile-parallel-in-background (progn (coq-par-enable) @@ -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) @@ -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' @@ -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 @@ -464,8 +464,8 @@ 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\".") @@ -477,10 +477,10 @@ 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 @@ -607,9 +607,9 @@ the second low the lower 16 bits of the time." (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 @@ -808,7 +808,7 @@ not backed by a file. The buffer to test must be current." (defun coq-compile-save-some-buffers () "Save buffers according to `coq-compile-auto-save'. -Uses the local variable ‘coq-compile-buffer-with-current-require’ to pass the +Uses the local variable `coq-compile-buffer-with-current-require' to pass the current buffer (which contains the Require command) to `coq-compile-save-buffer-filter'." (let ((coq-compile-buffer-with-current-require (current-buffer)) diff --git a/coq/coq-db.el b/coq/coq-db.el index 85aef62a1..fba1b077b 100644 --- a/coq/coq-db.el +++ b/coq/coq-db.el @@ -388,19 +388,19 @@ See `coq-syntax-db' for DB structure." (defconst coq-solve-tactics-face 'coq-solve-tactics-face "Expression that evaluates to a face. -Required so that \\='coq-solve-tactics-face is a proper facename") +Required so that \\+`coq-solve-tactics-face' is a proper facename") (defconst coq-cheat-face 'coq-cheat-face "Expression that evaluates to a face. -Required so that \\='coq-cheat-face is a proper facename") +Required so that \\+`coq-cheat-face' is a proper facename") (defconst coq-symbol-binder-face 'coq-symbol-binder-face "Expression that evaluates to a face. -Required so that \\='coq-symbol-binder-face is a proper facename") +Required so that \\+`coq-symbol-binder-face' is a proper facename") (defconst coq-symbol-face 'coq-symbol-face "Expression that evaluates to a face. -Required so that \\='coq-symbol-binder-face is a proper facename") +Required so that \\+`coq-symbol-binder-face' is a proper facename") (defconst coq-question-mark-face 'coq-question-mark-face) diff --git a/coq/coq-indent.el b/coq/coq-indent.el index 0b450993d..815dc5170 100644 --- a/coq/coq-indent.el +++ b/coq/coq-indent.el @@ -695,7 +695,7 @@ The point is put exactly before first non comment letter of the command." ;; (defun coq-find-unopened (&optional optlvl limit) ;; "Find the last unopened close item (looking forward from point). ;; Counter starts to OPTLVL (default 1) and stops when reaching -;; LIMIT (default ‘point-max’). This function only works inside an +;; LIMIT (default `point-max'). This function only works inside an ;; expression." ;; (let ((lvl (or optlvl 1)) after nextpt endpt) @@ -751,7 +751,7 @@ The point is put exactly before first non comment letter of the command." ;; (defun coq-end-offset (&optional limit) ;; "Find the first unclosed open indent item, and return its column. -;; Stop when reaching LIMIT (default to ‘point-min’)." +;; Stop when reaching LIMIT (default to `point-min')." ;; (save-excursion ;; (let ((found nil) ;; (anyreg (proof-regexp-alt "\\`" proof-indent-any-regexp))) diff --git a/coq/coq-local-vars.el b/coq/coq-local-vars.el index 892130f99..6d433fb0a 100644 --- a/coq/coq-local-vars.el +++ b/coq/coq-local-vars.el @@ -50,8 +50,8 @@ coqtop -foo3 -R foo bar -I foo2 FILE VARIABLES If for some reason you want to avoid or override the project file -method, you can use the file variables. See Info node ‘(emacs)File -Variables’. This feature of Emacs allows to set Emacs variables on a +method, you can use the file variables. See Info node `(emacs)File +Variables'. This feature of Emacs allows to set Emacs variables on a per-file basis. File Variables are (usually) written as a list at the end of the file. diff --git a/coq/coq-mode.el b/coq/coq-mode.el index 1f875e3da..2d7164a97 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) diff --git a/coq/coq-par-compile.el b/coq/coq-par-compile.el index 0a08fcc10..967b234a1 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) @@ -2372,7 +2372,7 @@ the ancestor hash are reinitialized. 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 +old last compilation job or put back into `proof-action-list'. The remaining batches of items that each start with a Require are then processed by `coq-par-handle-require-list', which creates require jobs as necessary. Before processing the diff --git a/coq/coq-seq-compile.el b/coq/coq-seq-compile.el index 42f93c36b..61cfad9c4 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 dbf032a60..290f5937d 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-syntax.el b/coq/coq-syntax.el index ed161cf74..8fea21d21 100644 --- a/coq/coq-syntax.el +++ b/coq/coq-syntax.el @@ -1049,7 +1049,7 @@ Used by `coq-goal-command-p'" ;; unused anymore (for good) (defun coq-goal-command-str-p (str) "Decide syntactically whether STR is a goal start or not. -Use ‘coq-goal-command-p’ on a span instead if possible." +Use `coq-goal-command-p' on a span instead if possible." (let* ((match (coq-count-match "\\_" str)) (with (- (coq-count-match "\\_" str) (coq-count-match "\\_" str))) (letwith (+ (coq-count-match "\\_" str) (- with match))) diff --git a/coq/coq-system.el b/coq/coq-system.el index 933c1594b..e9b3acd7f 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 953becf08..f9b25eae2 100644 --- a/coq/coq.el +++ b/coq/coq.el @@ -382,7 +382,7 @@ It is mostly useful in three window mode, see also ;; would not be shown in response buffer. If it is before, then we want it ;; urgent so that it is displayed. (defvar coq-eager-no-urgent-regex "\\s-*Finished " - "Regexp of commands matching ‘proof-shell-eager-annotation-start’ + "Regexp of commands matching `proof-shell-eager-annotation-start' that should maybe not be classified as urgent messages.") ;; return the end position if found, nil otherwise @@ -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,8 +987,8 @@ 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 -does not trigger ‘proof-shell-empty-action’ (which does \"Show\" at +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 running silent." @@ -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) @@ -1775,7 +1775,7 @@ hiding to be maintain when scripting/undoing." (defun coq-fold-hyp (h) "Fold hypothesis H's type from the context durably. \(displays \".......\" instead). This function relies on variable -‘coq-hyps-positions’. The hiding maintained as the goals buffer is +`coq-hyps-positions'. The hiding maintained as the goals buffer is changed, thanks to a hook on `proof-shell-handle-delayed-output-hook', consider using `coq-fold-hyp' if you want the hiding to be maintain when scripting/undoing." @@ -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/doc/PG-adapting.texi b/doc/PG-adapting.texi index ab474bc53..b9ca6d68c 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -337,9 +337,9 @@ more details. @c TEXI DOCSTRING MAGIC: proof-assistant-table @defvar proof-assistant-table Proof General's table of supported proof assistants.@* -This is copied from @samp{@code{proof-assistant-table-default}} at load time, +This is copied from @code{proof-assistant-table-default} at load time, removing any entries that do not have a corresponding directory -under @samp{@code{proof-home-directory}}. +under @code{proof-home-directory}. Each entry is a list of the form @lisp @@ -351,7 +351,7 @@ assistant, @samp{SYMBOL-mode}, run when files with @var{automode-regexp} (or with extension @var{file-extension}) are visited. If present, @var{ignored-extensions-list} is a list of file-name extensions to be ignored when doing file-name completion (@var{ignored-extensions-list} -is added to @samp{@code{completion-ignored-extensions}}). +is added to @code{completion-ignored-extensions}). @var{symbol} is also used to form the name of the directory and elisp file for the mode, which will be @@ -359,7 +359,7 @@ file for the mode, which will be @var{proof-home-directory}/@var{symbol}/@var{symbol}.el @end lisp where @var{proof-home-directory} is the value of the -variable @samp{@code{proof-home-directory}}. +variable @code{proof-home-directory}. @end defvar @@ -561,14 +561,14 @@ menu. @defvar PA-menu-entries Extra entries for proof assistant specific menu.@* A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation -of @samp{@code{easy-menu-define}} for more details. +of @code{easy-menu-define} for more details. @end defvar @c TEXI DOCSTRING MAGIC: PA-help-menu-entries @defvar PA-help-menu-entries Extra entries for help submenu for proof assistant specific help menu.@* A list of menu items [@var{name} @var{callback} @var{enabler} ...]. See the documentation -of @samp{@code{easy-menu-define}} for more details. +of @code{easy-menu-define} for more details. @end defvar @@ -618,7 +618,7 @@ If @var{menuname} is nil, item will not appear on the scripting menu. If @var{toolbar-p} is nil, item will not appear on the toolbar. -The default value is @samp{@code{proof-toolbar-entries-default}} which contains +The default value is @code{proof-toolbar-entries-default} which contains the standard Proof General buttons. @end defvar @@ -678,9 +678,9 @@ functions. String that terminates commands sent to prover; nil if none. To configure command recognition properly, you must set at least one -of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, -@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}}, -or @samp{@code{proof-script-parse-function}}. +of these: @code{proof-script-sexp-commands}, @code{proof-script-command-end-regexp}, +@code{proof-script-command-start-regexp}, @code{proof-terminal-string}, +or @code{proof-script-parse-function}. @end defvar @c TEXI DOCSTRING MAGIC: proof-electric-terminator-noterminator @@ -689,13 +689,13 @@ If non-nil, electric terminator does not actually insert a terminator. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-sexp-commands @defvar proof-script-sexp-commands -Non-nil if script has Lisp-like syntax: commands are @code{top-level} sexps.@* +Non-nil if script has Lisp-like syntax: commands are top-level sexps.@* You should set this variable in script mode configuration. To configure command recognition properly, you must set at least one -of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, -@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}}, -or @samp{@code{proof-script-parse-function}}. +of these: @code{proof-script-sexp-commands}, @code{proof-script-command-end-regexp}, +@code{proof-script-command-start-regexp}, @code{proof-terminal-string}, +or @code{proof-script-parse-function}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-command-start-regexp @@ -704,9 +704,9 @@ Regular expression which matches start of commands in proof script.@* You should set this variable in script mode configuration. To configure command recognition properly, you must set at least one -of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, -@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}}, -or @samp{@code{proof-script-parse-function}}. +of these: @code{proof-script-sexp-commands}, @code{proof-script-command-end-regexp}, +@code{proof-script-command-start-regexp}, @code{proof-terminal-string}, +or @code{proof-script-parse-function}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-command-end-regexp @@ -719,12 +719,12 @@ of this regexp. The regexp may include a nested group, which can be used to recognize the start of the following command (or white space). If there is a nested group, the end of the command is considered to be the start of the nested group, -i.e. (@code{match-beginning} 1), rather than (@code{match-end} 0). +i.e. (match-beginning 1), rather than (match-end 0). To configure command recognition properly, you must set at least one -of these: @samp{@code{proof-script-sexp-commands}}, @samp{@code{proof-script-command-end-regexp}}, -@samp{@code{proof-script-command-start-regexp}}, @samp{@code{proof-terminal-string}}, -or @samp{@code{proof-script-parse-function}}. +of these: @code{proof-script-sexp-commands}, @code{proof-script-command-end-regexp}, +@code{proof-script-command-start-regexp}, @code{proof-terminal-string}, +or @code{proof-script-parse-function}. @end defvar @@ -736,29 +736,29 @@ Read the Elisp manual (@pxref{Syntax Tables,,,Elisp}) for details about that. @c TEXI DOCSTRING MAGIC: proof-script-comment-start @defvar proof-script-comment-start String which starts a comment in the proof assistant command language.@* -The script buffer's @samp{@code{comment-start}} is set to this string plus a space. +The script buffer's @code{comment-start} is set to this string plus a space. Moreover, comments are usually ignored during script management, and not sent to the proof process. You should set this variable for reliable working of Proof General, -as well as @samp{@code{proof-script-comment-end}}. +as well as @code{proof-script-comment-end}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-comment-start-regexp @defvar proof-script-comment-start-regexp Regexp which matches a comment start in the proof command language. -The default value for this is set as (@code{regexp-quote} @samp{@code{proof-script-comment-start}}) +The default value for this is set as (regexp-quote @code{proof-script-comment-start}) but you can set this variable to something else more precise if necessary. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-comment-end @defvar proof-script-comment-end String which ends a comment in the proof assistant command language.@* -Should be an empty string if comments are terminated by @samp{@code{end-of-line}} -The script buffer's @samp{@code{comment-end}} is set to a space plus this string, +Should be an empty string if comments are terminated by @code{end-of-line} +The script buffer's @code{comment-end} is set to a space plus this string, if it is non-empty. -See also @samp{@code{proof-script-comment-start}}. +See also @code{proof-script-comment-start}. You should set this variable for reliable working of Proof General. @end defvar @@ -767,16 +767,16 @@ You should set this variable for reliable working of Proof General. @defvar proof-script-comment-end-regexp Regexp which matches a comment end in the proof command language. -The default value for this is set as (@code{regexp-quote} @samp{@code{proof-script-comment-end}}) +The default value for this is set as (regexp-quote @code{proof-script-comment-end}) but you can set this variable to something else more precise if necessary. @end defvar @c TEXI DOCSTRING MAGIC: proof-case-fold-search @defvar proof-case-fold-search -Value for @samp{@code{case-fold-search}} when recognizing portions of proof scripts.@* -Also used for completion, via @samp{@code{proof-script-complete}}. +Value for @code{case-fold-search} when recognizing portions of proof scripts.@* +Also used for completion, via @code{proof-script-complete}. The default value is nil. If your prover has a case @strong{insensitive} -input syntax, @samp{@code{proof-case-fold-search}} should be set to t instead. +input syntax, @code{proof-case-fold-search} should be set to t instead. NB: This setting is not used for matching output from the prover. @end defvar @@ -789,9 +789,9 @@ override this with a system-specific function. @c TEXI DOCSTRING MAGIC: proof-looking-at-syntactic-context @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 @code{'string}). +If so, return a symbol indicating this (@code{comment} or @code{string}). This function invokes if that is defined, otherwise -it calls @samp{@code{proof-looking-at-syntactic-context}}. +it calls @code{proof-looking-at-syntactic-context}. @end defun @node Recognizing proofs @section Recognizing proofs @@ -810,7 +810,7 @@ nested proofs; the present state is only part of the way there). @c TEXI DOCSTRING MAGIC: proof-goal-command-regexp @defvar proof-goal-command-regexp Matches a goal command in the proof script.@* -This is used to make the default value for @samp{@code{proof-goal-command-p}}, +This is used to make the default value for @code{proof-goal-command-p}, used as an important part of script management to find the start of an atomic undo block. @end defvar @@ -819,10 +819,10 @@ of an atomic undo block. @defvar proof-goal-command-p A function to test: is this really a goal command span? -This is added as a more refined addition to @samp{@code{proof-goal-command-regexp}}, +This is added as a more refined addition to @code{proof-goal-command-regexp}, to solve the problem that Coq and some other provers can have goals which look like definitions, etc. (In the future we may generalize -@samp{@code{proof-goal-command-regexp}} instead). +@code{proof-goal-command-regexp} instead). @end defvar @@ -830,8 +830,8 @@ look like definitions, etc. (In the future we may generalize @defvar proof-goal-with-hole-regexp Regexp which matches a command used to issue and name a goal.@* The name of the theorem is built from the variable -@samp{@code{proof-goal-with-hole-result}} using the same convention as -for @samp{@code{query-replace-regexp}}. +@code{proof-goal-with-hole-result} using the same convention as +for @code{query-replace-regexp}. Used for setting names of goal..save regions and for default configuration of other modes (function menu, imenu). @@ -840,10 +840,10 @@ It's safe to leave this setting as nil. @c TEXI DOCSTRING MAGIC: proof-goal-with-hole-result @defvar proof-goal-with-hole-result -How to get theorem name after @samp{@code{proof-goal-with-hole-regexp}} match.@* +How to get theorem name after @code{proof-goal-with-hole-regexp} match.@* String or Int. -If an int N, use @samp{@code{match-string}} to get the value of the Nth parenthesis matched. -If a string, use @samp{@code{replace-match}}. In this case, @samp{@code{proof-goal-with-hole-regexp}} +If an int N, use @code{match-string} to get the value of the Nth parenthesis matched. +If a string, use @code{replace-match}. In this case, @code{proof-goal-with-hole-regexp} should match the entire command. @end defvar @@ -856,8 +856,8 @@ Matches a save command. @defvar proof-save-with-hole-regexp Regexp which matches a command to save a named theorem.@* The name of the theorem is built from the variable -@samp{@code{proof-save-with-hole-result}} using the same convention as -@samp{@code{query-replace-regexp}}. +@code{proof-save-with-hole-result} using the same convention as +@code{query-replace-regexp}. Used for setting names of goal..save and proof regions. It's safe to leave this setting as nil. @@ -876,14 +876,14 @@ off the goal..[save] region in more flexible ways. The possibilities are: @lisp nil - nothing special; close only when a save arrives - @code{'closeany} - close as soon as the next command arrives, save or not - @code{'closegoal} - close when the next "goal" command arrives - @code{'extend} - keep extending the closed region until a save or goal. + @code{closeany} - close as soon as the next command arrives, save or not + @code{closegoal} - close when the next "goal" command arrives + @code{extend} - keep extending the closed region until a save or goal. @end lisp 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: @code{'extend} behaviour is not currently compatible with appearance of +NB: @code{extend} behaviour is not currently compatible with appearance of save commands, so don't use that if your prover has save commands. @end defvar @@ -891,7 +891,7 @@ save commands, so don't use that if your prover has save commands. @defvar proof-really-save-command-p Is this really a save command? -This is a more refined addition to @samp{@code{proof-save-command-regexp}}. +This is a more refined addition to @code{proof-save-command-regexp}. It should be a function taking a span and command as argument, and can be used to track nested proofs. @end defvar @@ -909,7 +909,7 @@ setting based on @code{proof-goal-with-hole-regexp} is configured. @c TEXI DOCSTRING MAGIC: proof-script-imenu-generic-expression @defvar proof-script-imenu-generic-expression Regular expressions to help find definitions and proofs in a script.@* -Value for @samp{@code{imenu-generic-expression}}, see documentation of Imenu +Value for @code{imenu-generic-expression}, see documentation of Imenu and that variable for details. @end defvar @@ -972,8 +972,8 @@ Regular expression matching commands which are @strong{not} undoable.@* These are commands which should not appear in proof scripts, for example, undo commands themselves (if the proof assistant cannot "redo" an "undo"). -Used in default functions @samp{@code{proof-generic-state-preserving-p}} -and @samp{@code{proof-generic-count-undos}}. If you don't use those, +Used in default functions @code{proof-generic-state-preserving-p} +and @code{proof-generic-count-undos}. If you don't use those, may be left as nil. @end defvar @@ -986,8 +986,8 @@ undo steps to issue. If this is set to a function, it should return a list of the appropriate commands (given the number of undo steps). -This setting is used for the default @samp{@code{proof-generic-count-undos}}. -If you set @samp{@code{proof-count-undos-fn}} to some other function, there is no +This setting is used for the default @code{proof-generic-count-undos}. +If you set @code{proof-count-undos-fn} to some other function, there is no need to set this variable. @end defvar @@ -995,8 +995,8 @@ need to set this variable. @defvar proof-ignore-for-undo-count Matcher for script commands to be ignored in undo count.@* May be left as nil, in which case it will be set to -@samp{@code{proof-non-undoables-regexp}}. -Used in default function @samp{@code{proof-generic-count-undos}}. +@code{proof-non-undoables-regexp}. +Used in default function @code{proof-generic-count-undos}. @end defvar @c TEXI DOCSTRING MAGIC: proof-count-undos-fn @@ -1006,20 +1006,20 @@ The function takes a span as an argument, and should return a string which is the command to undo to the target span. The target is guaranteed to be within the current (open) proof. This is an important function for script management. -The default setting @samp{@code{proof-generic-count-undos}} is based on the -settings @samp{@code{proof-non-undoables-regexp}} and -@samp{@code{proof-non-undoables-regexp}}. +The default setting @code{proof-generic-count-undos} is based on the +settings @code{proof-non-undoables-regexp} and +@code{proof-non-undoables-regexp}. @end defvar @c TEXI DOCSTRING MAGIC: proof-generic-count-undos @defun proof-generic-count-undos span Count number of undos in @var{span}, return commands needed to undo that far.@* -Command is set using @samp{@code{proof-undo-n-times-cmd}}. +Command is set using @code{proof-undo-n-times-cmd}. -A default value for @samp{@code{proof-count-undos-fn}}. +A default value for @code{proof-count-undos-fn}. For this function to work properly, you must configure -@samp{@code{proof-undo-n-times-cmd}} and @samp{@code{proof-ignore-for-undo-count}}. +@code{proof-undo-n-times-cmd} and @code{proof-ignore-for-undo-count}. @end defun @@ -1033,14 +1033,14 @@ Function to return list of commands to forget to before its argument span.@* 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 (@code{proof-unprocessed-begin}). This may involve forgetting a number +up to @code{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. This is an important function for script management. Study one of the existing instantiations for examples of how to write it, -or leave it set to the default function @samp{@code{proof-generic-find-and-forget}} +or leave it set to the default function @code{proof-generic-find-and-forget} (which see). @end defvar @@ -1052,8 +1052,8 @@ open goal at the moment, so forgetting involves unbinding declarations, etc, rather than undoing proof steps. This generic implementation assumes it is enough to find the -nearest following span with a @samp{name} property, and retract -that using @samp{@code{proof-forget-id-command}} with the given name. +nearest following span with a @code{name} property, and retract +that using @code{proof-forget-id-command} with the given name. If this behaviour is not correct, you must customize the function with something different. @@ -1064,9 +1064,9 @@ with something different. Command to forget back to a given named span.@* A string; @samp{%s} will be replaced by the name of the span. -This is only used in the implementation of @samp{@code{proof-generic-find-and-forget}}, +This is only used in the implementation of @code{proof-generic-find-and-forget}, you only need to set if you use that function (by not customizing -@samp{@code{proof-find-and-forget-fn}}. +@code{proof-find-and-forget-fn}. @end defvar @c TEXI DOCSTRING MAGIC: pg-topterm-goalhyplit-fn @@ -1074,7 +1074,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, @code{'goal'}, @code{'hyp'} or @code{'lit'}. +First element of the cons is a symbol, @code{goal}, @code{hyp} or @code{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 @@ -1085,13 +1085,13 @@ will be attempted. @defvar proof-kill-goal-command Command to kill the currently open goal. -If this is set to nil, PG will expect @samp{@code{proof-find-and-forget-fn}} +If this is set to nil, PG will expect @code{proof-find-and-forget-fn} to do all the work of retracting to an arbitrary point in a file. Otherwise, the generic split-phase mechanism will be used: -1. If inside an unclosed proof, use @samp{proof-count-undos}. +1. If inside an unclosed proof, use @code{proof-count-undos}. 2. If retracting to before an unclosed proof, use -@samp{@code{proof-kill-goal-command}}, followed by @samp{@code{proof-find-and-forget-fn}} +@code{proof-kill-goal-command}, followed by @code{proof-find-and-forget-fn} if necessary. @end defvar @@ -1127,11 +1127,11 @@ Regexp for commands that must be counted in nested goal-save regions. 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 @code{'nestedundos} +At the moment, the behaviour is that a goal-save span has a @code{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 -@code{'nestedundos} setting. Coq uses this to forget declarations, since +@code{nestedundos} setting. Coq uses this to forget declarations, since declarations in Coq reside in a separate context with its own (flat) history. @end defvar @@ -1186,38 +1186,38 @@ configured. @c TEXI DOCSTRING MAGIC: proof-omit-proofs-configured @defvar proof-omit-proofs-configured 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 +See also @code{proof-omit-proofs-option} or the Proof General manual 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 -@samp{@code{proof-script-proof-admit-command}} have been configured. +all of @code{proof-script-proof-start-regexp}, +@code{proof-script-proof-end-regexp}, +@code{proof-script-definition-end-regexp} and +@code{proof-script-proof-admit-command} have been configured. The omit proofs feature skips over opaque proofs in the source code, admitting the theorems, to speed up processing. -If @samp{@code{proof-omit-proofs-option}} is set by the user, all proof +If @code{proof-omit-proofs-option} is set by the user, all proof 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 +@code{proof-script-proof-start-regexp} up to and including the next +match of @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-definition-end-regexp}} is found while searching +@code{proof-script-proof-admit-command}. If a match for +@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 +@code{proof-script-cmd-prevents-proof-omission} recognizes a proof command that prevents proof omission then the current proof (up to and including the match of -@samp{@code{proof-script-definition-end-regexp}} or -@samp{@code{proof-script-proof-end-regexp}}) is considered to be not opaque +@code{proof-script-definition-end-regexp} or +@code{proof-script-proof-end-regexp}) is considered to be not opaque 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 -@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 +@code{proof-script-proof-start-regexp} is found before the next match +for @code{proof-script-proof-end-regexp} or +@code{proof-script-definition-end-regexp}, the search for opaque proofs immediately stops and all commands following the previous -match of @samp{@code{proof-script-proof-start-regexp}} are sent verbatim to +match of @code{proof-script-proof-start-regexp} are sent verbatim to the proof assistant. All the regular expressions for this feature are matched against @@ -1228,19 +1228,19 @@ without surrounding space. @c TEXI DOCSTRING MAGIC: proof-script-proof-start-regexp @defvar proof-script-proof-start-regexp Regular expression for the start of a proof for the omit proofs feature.@* -See @samp{@code{proof-omit-proofs-configured}}. +See @code{proof-omit-proofs-configured}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-proof-end-regexp @defvar proof-script-proof-end-regexp Regular expression for the end of an opaque proof for the omit proofs feature.@* -See @samp{@code{proof-omit-proofs-configured}}. +See @code{proof-omit-proofs-configured}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-definition-end-regexp @defvar proof-script-definition-end-regexp Regexp for the end of a non-opaque proof for the omit proofs feature.@* -See @samp{@code{proof-omit-proofs-configured}}. +See @code{proof-omit-proofs-configured}. @end defvar @c TEXI DOCSTRING MAGIC: proof-script-proof-admit-command @@ -1268,7 +1268,7 @@ matches proof-script commands that prevent the omission of proofs 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 -command matches @samp{@code{proof-script-proof-start-regexp}} this following +command matches @code{proof-script-proof-start-regexp} this following proof will not be omitted. Note that recognition of commands with this regular expression @@ -1303,8 +1303,8 @@ 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 +Return proof name and state number for @code{proof-check-proofs}.@* +Proof assistant specific function for @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 @@ -1314,20 +1314,20 @@ the following order: * the name of the current proof (as string) or nil The proof assistant should return to the same state when the -state number is supplied to @samp{@code{proof-retract-command-fn}}. -Processing the command returned by @samp{@code{proof-retract-command-fn}} +state number is supplied to @code{proof-retract-command-fn}. +Processing the command returned by @code{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 -@samp{@code{proof-tree-get-proof-info}}.) +@code{proof-tree-get-proof-info}.) @end defvar @c TEXI DOCSTRING MAGIC: proof-retract-command-fn @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 +@code{proof-get-proof-info-fn}. It should return a command that brings the proof assistant back to the same state. @end defvar @@ -1353,16 +1353,16 @@ assistant (with respect to an on-going proof). @c TEXI DOCSTRING MAGIC: proof-state-preserving-p @defvar proof-state-preserving-p A predicate, non-nil if its argument (a command) preserves the proof state.@* -This is a safety-test used by @samp{@code{proof-minibuffer-cmd}} to filter out scripting +This is a safety-test used by @code{proof-minibuffer-cmd} to filter out scripting commands which should be entered directly into the script itself. -The default setting for this function, @samp{@code{proof-generic-state-preserving-p}} -tests by negating the match on @samp{@code{proof-non-undoables-regexp}}. +The default setting for this function, @code{proof-generic-state-preserving-p} +tests by negating the match on @code{proof-non-undoables-regexp}. @end defvar @c TEXI DOCSTRING MAGIC: proof-generic-state-preserving-p @defun proof-generic-state-preserving-p cmd -Is @var{cmd} state preserving? Match on @samp{@code{proof-non-undoables-regexp}}. +Is @var{cmd} state preserving? Match on @code{proof-non-undoables-regexp}. @end defun @@ -1381,8 +1381,8 @@ assistant, for example, to switch to a new theory script). When functions in this hook are called, the variable -@samp{activated-interactively} will be non-nil if -@samp{@code{proof-activate-scripting}} was called interactively +@code{activated-interactively} will be non-nil if +@code{proof-activate-scripting} was called interactively (rather than as a side-effect of some other action). If a hook function sends commands to the proof process, it should wait for them to complete (so the queue is cleared @@ -1469,14 +1469,14 @@ List of identifiers to use for completion for this proof assistant.@* Completion is activated with M-x complete. If this table is empty or needs adjusting, please make changes using -@samp{@code{customize-variable}} and post suggestions at +@code{customize-variable} and post suggestions at https://github.com/ProofGeneral/PG/issues @end defvar @c TEXI DOCSTRING MAGIC: proof-add-completions @deffn Command proof-add-completions Add completions from -completion-table to completion database.@* -Uses @samp{@code{add-completion}} with a negative number of uses and ancient +Uses @code{add-completion} with a negative number of uses and ancient last use time, to discourage saving these into the users database. @end deffn @@ -1528,16 +1528,16 @@ System command to run the proof assistant in the proof shell.@* May contain arguments separated by spaces, but see also the prover specific settings @samp{-prog-args} and @samp{-prog-env}. -Remark: if @samp{-prog-args} is non-nil, then @samp{@code{proof-prog-name}} is considered +Remark: if @samp{-prog-args} is non-nil, then @code{proof-prog-name} is considered strictly: it must contain @strong{only} the program name with no option, spaces are interpreted literally as part of the program name. @end defvar @c TEXI DOCSTRING MAGIC: PA-prog-args @defvar PA-prog-args -Arguments to be passed to @samp{@code{proof-prog-name}} to run the proof assistant.@* -If non-nil, will be treated as a list of arguments for @samp{@code{proof-prog-name}}. -Otherwise @samp{@code{proof-prog-name}} will be split on spaces to form arguments. +Arguments to be passed to @code{proof-prog-name} to run the proof assistant.@* +If non-nil, will be treated as a list of arguments for @code{proof-prog-name}. +Otherwise @code{proof-prog-name} will be split on spaces to form arguments. Remark: Arguments are interpreted strictly: each one must contain only one word, with no space (unless it is the same word). For example if the @@ -1547,20 +1547,20 @@ arguments are -x foo -y bar, then the list should be '("-x" "foo" @c TEXI DOCSTRING MAGIC: PA-prog-env @defvar PA-prog-env -Modifications to @samp{@code{process-environment}} made before running @samp{@code{proof-prog-name}}.@* +Modifications to @code{process-environment} made before running @code{proof-prog-name}.@* Each element should be a string of the form ENVVARNAME=@var{value}. They will be added to the environment before launching the prover (but not pervasively). For example for coq on Windows you might need something like: -(setq @code{coq-prog-env} '("HOME=C:\Program Files\Coq\")) +(setq coq-prog-env '("HOME=C:\Program Files\Coq\")) @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-auto-terminate-commands @defvar proof-shell-auto-terminate-commands Non-nil if Proof General should try to add terminator to every command.@* If non-nil, whenever a command is sent to the prover using -@samp{@code{proof-shell-invisible-command}}, Proof General will check to see if it -ends with @samp{@code{proof-terminal-string}}, and add it if not. -If @samp{@code{proof-terminal-string}} is nil, this has no effect. +@code{proof-shell-invisible-command}, Proof General will check to see if it +ends with @code{proof-terminal-string}, and add it if not. +If @code{proof-terminal-string} is nil, this has no effect. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-pre-sync-init-cmd @@ -1574,7 +1574,7 @@ It is better to configure the proof assistant for this purpose via command line options if possible, in which case this variable does not need to be set. -See also @samp{@code{proof-shell-init-cmd}}. +See also @code{proof-shell-init-cmd}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-init-cmd @@ -1585,7 +1585,7 @@ This command is sent to the process as soon as synchronization is gained the proof assistant in some way, or print a welcome message (since output before the first prompt is discarded). -See also @samp{@code{proof-shell-pre-sync-init-cmd}}. +See also @code{proof-shell-pre-sync-init-cmd}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-restart-cmd @@ -1602,15 +1602,15 @@ A command to quit the proof process. If nil, send EOF instead. @defvar proof-shell-cd-cmd Command to the proof assistant to change the working directory.@* The format character @samp{%s} is replaced with the directory, and -the escape sequences in @samp{@code{proof-shell-filename-escapes}} are +the escape sequences in @code{proof-shell-filename-escapes} are applied to the filename. -This setting is used to define the function @samp{@code{proof-cd}} which -changes to the value of (@code{default-directory}) for script buffers. -For files, the value of (@code{default-directory}) is simply the +This setting is used to define the function @code{proof-cd} which +changes to the value of @code{default-directory} for script buffers. +For files, the value of @code{default-directory} is simply the directory the file resides in. -NB: By default, @samp{@code{proof-cd}} is called from @samp{@code{proof-activate-scripting-hook}}, +NB: By default, @code{proof-cd} is called from @code{proof-activate-scripting-hook}, so that the prover switches to the directory of a proof script every time scripting begins. @end defvar @@ -1620,7 +1620,7 @@ script every time scripting begins. Command to turn prover goals output off when sending many script commands.@* If non-nil, Proof General will automatically issue this command to help speed up processing of long proof scripts. -See also @samp{@code{proof-shell-stop-silent-cmd}}. +See also @code{proof-shell-stop-silent-cmd}. NB: terminator not added to command. @end defvar @@ -1629,7 +1629,7 @@ NB: terminator not added to command. Command to turn prover output on.@* If non-nil, Proof General will automatically issue this command to help speed up processing of long proof scripts. -See also @samp{@code{proof-shell-start-silent-cmd}}. +See also @code{proof-shell-start-silent-cmd}. NB: Terminator not added to command. @end defvar @@ -1649,7 +1649,7 @@ for more details about the final two settings in this group, Command to the proof assistant to tell it that a file has been processed.@* The format character @samp{%s} is replaced by a complete filename for a script file which has been fully processed interactively with -Proof General. See @samp{@code{proof-format-filename}} for other possibilities +Proof General. See @code{proof-format-filename} for other possibilities to process the filename. This setting used to interface with the proof assistant's internal @@ -1661,15 +1661,15 @@ issuing this command. If this is set to nil, no command is issued. -See also: @samp{@code{proof-shell-inform-file-retracted-cmd}}, -@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}. +See also: @code{proof-shell-inform-file-retracted-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-inform-file-retracted-cmd @defvar proof-shell-inform-file-retracted-cmd Command to the proof assistant to tell it that a file has been retracted.@* The format character @samp{%s} is replaced by a complete filename for a script file which Proof General wants the prover to consider as not -completely processed. See @samp{@code{proof-format-filename}} for other +completely processed. See @code{proof-format-filename} for other possibilities to process the filename. This is used to interface with the proof assistant's internal @@ -1685,11 +1685,11 @@ If this is set to nil, no command is issued. It is also possible to set this value to a function which will be invoked on the name of the retracted file, and should remove -the ancestor files from @samp{@code{proof-included-files-list}} by some +the ancestor files from @code{proof-included-files-list} by some other calculation. -See also: @samp{@code{proof-shell-inform-file-processed-cmd}}, -@samp{@code{proof-shell-process-file}}, @samp{@code{proof-shell-compute-new-files-list}}. +See also: @code{proof-shell-inform-file-processed-cmd}, +@code{proof-shell-process-file}, @code{proof-shell-compute-new-files-list}. @end defvar @@ -1717,44 +1717,44 @@ input, then newlines can be retained in the input. @c TEXI DOCSTRING MAGIC: proof-shell-insert-hook @defvar proof-shell-insert-hook -Hook run by @samp{@code{proof-shell-insert}} before inserting a command.@* +Hook run by @code{proof-shell-insert} before inserting a command.@* Can be used to configure the proof assistant to the interface in various ways -- for example, to observe or alter the commands sent to the prover, or to sneak in extra commands to configure the prover. -This hook is called inside a @samp{@code{save-excursion}} with the @samp{@code{proof-shell-buffer}} +This hook is called inside a @code{save-excursion} with the @code{proof-shell-buffer} current, just before inserting and sending the text in the -variable @samp{string}. The hook can massage @samp{string} or insert additional -text directly into the @samp{@code{proof-shell-buffer}}. -Before sending @samp{string}, it will be stripped of carriage returns. +variable @code{string}. The hook can massage @code{string} or insert additional +text directly into the @code{proof-shell-buffer}. +Before sending @code{string}, it will be stripped of carriage returns. -Additionally, the hook can examine the variable @samp{action}. It will be +Additionally, the hook can examine the variable @code{action}. It will be a symbol, set to the callback command which is executed in the proof -shell filter once @samp{string} has been processed. The @samp{action} variable +shell filter once @code{string} has been processed. The @code{action} variable suggests what class of command is about to be inserted, the first two are normally the ones of interest: @lisp - @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 suppressed - @code{'proof-shell-clear-silent} Indicates prover output has been restored - @code{'init-cmd} Early initialization command sent to prover + @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 suppressed + @code{proof-shell-clear-silent} Indicates prover output has been restored + @code{init-cmd} Early initialization command sent to prover @end lisp Caveats: You should be very careful about setting this hook. Proof General relies on a careful synchronization with the process between inputs and outputs. It expects to see a prompt for each input it sends from the queue. If you add extra input here and it causes more prompts than expected, things will break! Extending the variable -@samp{string} may be safer than inserting text directly, since it is +@code{string} may be safer than inserting text directly, since it is stripped of carriage returns before being sent. Example uses: Lego used this hook for setting the pretty printer width if the window width has changed; -Plastic used it to remove literate-style markup from @samp{string}. +Plastic used it to remove literate-style markup from @code{string}. -See also @samp{@code{proof-script-preprocess}} which can munge text when +See also @code{proof-script-preprocess} which can munge text when it is added to the queue of commands. @end defvar @@ -1801,15 +1801,15 @@ Regexp matching an error report from the proof assistant. We assume that an error message corresponds to a failure in the last proof command executed. So don't match mere warning messages with this regexp. Moreover, an error message should @strong{not} be matched as an -eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it will be lost. -Error messages are considered to begin from @samp{@code{proof-shell-error-regexp}} +Error messages are considered to begin from @code{proof-shell-error-regexp} and continue until the next prompt. The variable -@samp{@code{proof-shell-truncate-before-error}} controls whether text before the +@code{proof-shell-truncate-before-error} controls whether text before the error message is displayed. -The engine matches interrupts before errors, see @samp{@code{proof-shell-interrupt-regexp}}. +The engine matches interrupts before errors, see @code{proof-shell-interrupt-regexp}. It is safe to leave this variable unset (as nil). @end defvar @@ -1819,10 +1819,10 @@ Regexp matching output indicating the assistant was interrupted.@* We assume that an interrupt message corresponds to a failure in the last proof command executed. So don't match mere warning messages with this regexp. Moreover, an interrupt message should not be matched as an -eager annotation (see @samp{@code{proof-shell-eager-annotation-start}}) otherwise it +eager annotation (see @code{proof-shell-eager-annotation-start}) otherwise it will be lost. -The engine matches interrupts before errors, see @samp{@code{proof-shell-error-regexp}}. +The engine matches interrupts before errors, see @code{proof-shell-error-regexp}. It is safe to leave this variable unset (as nil). @end defvar @@ -1838,7 +1838,7 @@ behaviour in Proof General before version 3.4. The more obvious setting for new instances is probably nil. Interrupt messages are treated in the same way. -See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt-regexp}}. +See @code{proof-shell-error-regexp} and @code{proof-shell-interrupt-regexp}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-proof-completed-regexp @@ -1846,7 +1846,7 @@ See @samp{@code{proof-shell-error-regexp}} and @samp{@code{proof-shell-interrupt Regexp matching output indicating a finished proof. When output which matches this regexp is seen, we clear the goals -buffer in case this is not also marked up as a @samp{goals} type of +buffer in case this is not also marked up as a @code{goals} type of message. We also enable the QED function (save a proof) and we may automatically @@ -1856,14 +1856,14 @@ command, depending on whether the prover supports nested proofs or not. @c TEXI DOCSTRING MAGIC: proof-shell-start-goals-regexp @defvar proof-shell-start-goals-regexp 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 +This is an important setting. Output between @code{proof-shell-start-goals-regexp} +and @code{proof-shell-end-goals-regexp} will be pasted into the goals buffer 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 regexp, unless it has a match group, in which case it starts -at (@code{match-end} 1). +at (match-end 1). @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-end-goals-regexp @defvar proof-shell-end-goals-regexp @@ -1872,11 +1872,11 @@ This allows a shorter form of the proof state output to be displayed, in case several messages are combined in a command output. The portion treated as the goals output will be that between the -match on @samp{@code{proof-shell-start-goals-regexp}} (which see) and the -start of the match on @samp{@code{proof-shell-end-goals-regexp}}. +match on @code{proof-shell-start-goals-regexp} (which see) and the +start of the match on @code{proof-shell-end-goals-regexp}. If nil, use the whole of the output from the match on -@samp{@code{proof-shell-start-goals-regexp}} up to the next prompt. +@code{proof-shell-start-goals-regexp} up to the next prompt. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-assumption-regexp @defvar proof-shell-assumption-regexp @@ -1884,7 +1884,7 @@ A regular expression matching the name of assumptions. At the moment, this setting is not used in the generic Proof General. -Future use may provide a generic implementation for @samp{@code{pg-topterm-goalhyplit-fn}}, +Future use may provide a generic implementation for @code{pg-topterm-goalhyplit-fn}, used to help parse the goals buffer to annotate it for proof by pointing. @end defvar @@ -1920,11 +1920,11 @@ are stripped from display of the message in the minibuffer. It is useful to recognize (starts of) warnings or file-reading messages with this regexp. You must also recognize any special messages -from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, -@samp{@code{proof-shell-retract-files-regexp}}, etc.) +from the prover to PG with this regexp (e.g. @code{proof-shell-clear-goals-regexp}, +@code{proof-shell-retract-files-regexp}, etc.) -See also @samp{@code{proof-shell-eager-annotation-start-length}}, -@samp{@code{proof-shell-eager-annotation-end}}. +See also @code{proof-shell-eager-annotation-start-length}, +@code{proof-shell-eager-annotation-end}. Set to nil to disable this feature. @end defvar @@ -1933,7 +1933,7 @@ Set to nil to disable this feature. @defvar proof-shell-eager-annotation-start-length Maximum length of an eager annotation start.@* Must be set to the maximum length of the text that may match -@samp{@code{proof-shell-eager-annotation-start}} (at least 1). +@code{proof-shell-eager-annotation-start} (at least 1). If this value is too low, eager annotations may be lost! This value is used internally by Proof General to optimize the process @@ -1946,12 +1946,12 @@ Eager annotation field end. A regular expression or nil.@* An eager annotation indicates to Emacs that some following output should be displayed or processed immediately. -See also @samp{@code{proof-shell-eager-annotation-start}}. +See also @code{proof-shell-eager-annotation-start}. It is nice to recognize (ends of) warnings or file-reading messages with this regexp. You must also recognize (ends of) any special messages -from the prover to PG with this regexp (e.g. @samp{@code{proof-shell-clear-goals-regexp}}, -@samp{@code{proof-shell-retract-files-regexp}}, etc.) +from the prover to PG with this regexp (e.g. @code{proof-shell-clear-goals-regexp}, +@code{proof-shell-retract-files-regexp}, etc.) The default value is "\n" to match up to the end of the line. @end defvar @@ -1970,8 +1970,8 @@ be acted on as soon as they are issued by the prover. Regexp matching output telling Proof General to clear the response buffer. More precisely, this should match a string which is bounded by -matches on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +matches on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. This feature is useful to give the prover more control over what output is shown to the user. Set to nil to disable. @@ -1982,8 +1982,8 @@ is shown to the user. Set to nil to disable. Regexp matching output telling Proof General to clear the goals buffer. More precisely, this should match a string which is bounded by -matches on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +matches on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. This feature is useful to give the prover more control over what output is shown to the user. Set to nil to disable. @@ -1999,8 +1999,8 @@ the shell buffer will be displayed and the user left to their own devices. Note: this should match a string which is bounded by matches -on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-trace-output-regexp @@ -2014,8 +2014,8 @@ This is intended for unusual debugging output from the prover, rather than ordinary output from final proofs. This should match a string which is bounded by matches -on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. Set to nil to disable. @end defvar @@ -2029,7 +2029,7 @@ The output from the prover should be a message with the form @var{dependencies} OF X Y Z ARE A B C @end lisp with X Y Z, A B C separated by whitespace or somehow else (see -@samp{@code{proof-shell-theorem-dependency-list-split}}. This variable should +@code{proof-shell-theorem-dependency-list-split}. This variable should be set to a regexp to match the overall message (which should be an urgent message), with two sub-matches for X Y Z and A B C. @@ -2056,13 +2056,13 @@ the empty string, the file name of the scripting buffer is used instead. If it returns nil, no action is taken. More precisely, @var{regexp} should match a string which is bounded by -matches on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +matches on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. Care has to be taken in case the prover only reports on compiled versions of files it is processing. In this case, @var{function} needs to reconstruct the corresponding script file name. The new (true) file -name is added to the front of @samp{@code{proof-included-files-list}}. +name is added to the front of @code{proof-included-files-list}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-retract-files-regexp @@ -2070,12 +2070,12 @@ name is added to the front of @samp{@code{proof-included-files-list}}. Matches a message that the prover has retracted a file. More precisely, this should match a string which is bounded by -matches on @samp{@code{proof-shell-eager-annotation-start}} and -@samp{@code{proof-shell-eager-annotation-end}}. +matches on @code{proof-shell-eager-annotation-start} and +@code{proof-shell-eager-annotation-end}. At this stage, Proof General's view of the processed files is out of date and needs to be updated with the help of the function -@samp{@code{proof-shell-compute-new-files-list}}. +@code{proof-shell-compute-new-files-list}. @end defvar @vindex proof-included-files-list @@ -2084,14 +2084,14 @@ date and needs to be updated with the help of the function Function to update @samp{proof-included-files list}. It needs to return an up-to-date list of all processed files. The -result will be stored in @samp{@code{proof-included-files-list}}. +result will be stored in @code{proof-included-files-list}. -This function is called when @samp{@code{proof-shell-retract-files-regexp}} +This function is called when @code{proof-shell-retract-files-regexp} has been matched in the prover output. In practice, this function is likely to inspect the -previous (global) variable @samp{@code{proof-included-files-list}} and the -match data triggered by @samp{@code{proof-shell-retract-files-regexp}}. +previous (global) variable @code{proof-included-files-list} and the +match data triggered by @code{proof-shell-retract-files-regexp}. @end defvar @@ -2130,12 +2130,12 @@ quote characters must be escaped. The setting @end lisp achieves this. -This setting is used inside the function @samp{@code{proof-format-filename}}. +This setting is used inside the function @code{proof-format-filename}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-process-connection-type @defvar proof-shell-process-connection-type -The value of @samp{@code{process-connection-type}} for the proof shell.@* +The value of @code{process-connection-type} for the proof shell.@* Set non-nil for ptys, nil for pipes. @var{note}: In Emacs >= 24 (checked for 24 and 25.0.50.1), t is not a @@ -2145,23 +2145,23 @@ good choice: input is cut after @var{4095} chars, which hangs pg. @c TEXI DOCSTRING MAGIC: proof-shell-handle-error-or-interrupt-hook @defvar proof-shell-handle-error-or-interrupt-hook Run after an error or interrupt has been reported in the response buffer.@* -Hook functions may inspect @samp{@code{proof-shell-last-output-kind}} to +Hook functions may inspect @code{proof-shell-last-output-kind} to determine whether the cause was an error or interrupt. Possible values for this hook include: @lisp - @samp{@code{proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window}} - @samp{@code{proof-goto-end-of-locked-if-pos-not-visible-in-window}} + @code{proof-goto-end-of-locked-on-error-if-pos-not-visible-in-window} + @code{proof-goto-end-of-locked-if-pos-not-visible-in-window} @end lisp which move the cursor in the scripting buffer on an error or error/interrupt. Remark: This hook is called from shell buffer. If you want to do -something in scripting buffer, @samp{@code{save-excursion}} and/or @samp{@code{set-buffer}}. +something in scripting buffer, @code{save-excursion} and/or @code{set-buffer}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-pre-interrupt-hook @defvar proof-shell-pre-interrupt-hook -Run immediately after @samp{@code{comint-interrupt-subjob}} is called.@* +Run immediately after @code{comint-interrupt-subjob} is called.@* This hook is added to allow customization for systems that query the user before returning to the top level. @end defvar @@ -2170,23 +2170,23 @@ before returning to the top level. @defvar proof-shell-handle-output-system-specific Set this variable to handle system specific output.@* 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 +@code{proof-shell-handle-immediate-output}. Later output is +handled by @code{proof-shell-handle-delayed-output}, which displays messages to the user in @strong{goals} and @strong{response} buffers. This hook can run between the two stages to take some effect. It should be a function which is passed (cmd string) as -arguments, where @samp{cmd} is a string containing the currently -processed command and @samp{string} is the response from the proof +arguments, where @code{cmd} is a string containing the currently +processed command and @code{string} is the response from the proof system. If action is taken and goals/response display should be prevented, the function should update the variable -@samp{@code{proof-shell-last-output-kind}} to some non-nil symbol. +@code{proof-shell-last-output-kind} to some non-nil symbol. The symbol will be compared against standard ones, see documentation -of @samp{@code{proof-shell-last-output-kind}}. A suggested canonical non-standard -symbol is @code{'systemspecific}. +of @code{proof-shell-last-output-kind}. A suggested canonical non-standard +symbol is @code{systemspecific}. @end defvar @@ -2223,28 +2223,28 @@ Regexp indicating that the proof process has identified an error. @c TEXI DOCSTRING MAGIC: proof-shell-result-start @defvar proof-shell-result-start Regexp matching start of an output from the prover after pbp commands.@* -In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +In particular, after a @code{pbp-goal-command} or a @code{pbp-hyp-command}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-result-end @defvar proof-shell-result-end Regexp matching end of output from the prover after pbp commands.@* -In particular, after a @samp{@code{pbp-goal-command}} or a @samp{@code{pbp-hyp-command}}. +In particular, after a @code{pbp-goal-command} or a @code{pbp-hyp-command}. @end defvar @c TEXI DOCSTRING MAGIC: pg-subterm-start-char @defvar pg-subterm-start-char Opening special character for subterm markup.@* Subsequent special characters with values @strong{below} -@samp{@code{pg-subterm-first-special-char}} are assumed to be subterm position -indicators. Annotations should be finished with @samp{@code{pg-subterm-sep-char}}; -the end of the concrete syntax is indicated by @samp{@code{pg-subterm-end-char}}. +@code{pg-subterm-first-special-char} are assumed to be subterm position +indicators. Annotations should be finished with @code{pg-subterm-sep-char}; +the end of the concrete syntax is indicated by @code{pg-subterm-end-char}. -If @samp{@code{pg-subterm-start-char}} is nil, subterm markup is disabled. +If @code{pg-subterm-start-char} is nil, subterm markup is disabled. @end defvar @c TEXI DOCSTRING MAGIC: pg-subterm-sep-char @defvar pg-subterm-sep-char Finishing special for a subterm markup.@* -See doc of @samp{@code{pg-subterm-start-char}}. +See doc of @code{pg-subterm-start-char}. @end defvar @c TEXI DOCSTRING MAGIC: pg-topterm-regexp @defvar pg-topterm-regexp @@ -2253,7 +2253,7 @@ A "top" element may be a sub-goal to be proved or a named hypothesis, for example. It could also be a literal command to insert and send back to the prover. -The function @samp{@code{pg-topterm-goalhyplit-fn}} examines text following this +The function @code{pg-topterm-goalhyplit-fn} examines text following this special character, to determine what kind of top element it is. This setting is also used to see if proof-by-pointing features @@ -2263,7 +2263,7 @@ for parsing the prover output is disabled. @c TEXI DOCSTRING MAGIC: pg-subterm-end-char @defvar pg-subterm-end-char Closing special character for subterm markup.@* -See @samp{@code{pg-subterm-start-char}}. +See @code{pg-subterm-start-char}. @end defvar @@ -2314,7 +2314,7 @@ The default value is @code{"https://proofgeneral.github.io"}. @defvar proof-universal-keys List of key bindings made for all proof general buffers.@* Elements of the list are tuples @samp{(k . f)} -where @samp{k} is a key binding (vector) and @samp{f} the designated function. +where @code{k} is a key binding (vector) and @code{f} the designated function. @end defvar @@ -2346,12 +2346,12 @@ will be allowed (unless @code{proof-strict-read-only} allows it). @defvar proof-included-files-list List of files currently included in proof process.@* This list contains files in canonical truename format -(see @samp{@code{file-truename}}). +(see @code{file-truename}). Whenever a new file is being processed, it gets added to this list -via the @samp{@code{proof-shell-process-file}} configuration settings. +via the @code{proof-shell-process-file} configuration settings. When the prover retracts a file, this list is resynchronised via the -@samp{@code{proof-shell-retract-files-regexp}} and @samp{@code{proof-shell-compute-new-files-list}} +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} configuration settings. Only files which have been @strong{fully} processed should be included here. @@ -2507,10 +2507,10 @@ A flat list of the form @lisp (@var{char} @var{syncode} @var{char} @var{syncode} ...) @end lisp -See doc of @samp{@code{modify-syntax-entry}} for details of characters +See doc of @code{modify-syntax-entry} for details of characters and syntax codes. -At present this is used only by the @samp{@code{proof-easy-config}} macro. +At present this is used only by the @code{proof-easy-config} macro. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-syntax-table-entries @defvar proof-shell-syntax-table-entries @@ -2519,10 +2519,10 @@ A flat list of the form @lisp (@var{char} @var{syncode} @var{char} @var{syncode} ...) @end lisp -See doc of @samp{@code{modify-syntax-entry}} for details of characters +See doc of @code{modify-syntax-entry} for details of characters and syntax codes. -At present this is used only by the @samp{@code{proof-easy-config}} macro. +At present this is used only by the @code{proof-easy-config} macro. @end defvar Some additional useful settings are: @@ -2567,24 +2567,24 @@ Proof General, @pxref{Demonstration instance and easy configuration}. @c TEXI DOCSTRING MAGIC: proof-script-font-lock-keywords @defvar proof-script-font-lock-keywords -Value of @samp{@code{font-lock-keywords}} used to fontify proof scripts.@* -The proof script mode should set this before calling @samp{@code{proof-config-done}}. -Used also by @samp{@code{proof-easy-config}} mechanism. -See also @samp{@code{proof-goals-font-lock-keywords}} and @samp{@code{proof-response-font-lock-keywords}}. +Value of @code{font-lock-keywords} used to fontify proof scripts.@* +The proof script mode should set this before calling @code{proof-config-done}. +Used also by @code{proof-easy-config} mechanism. +See also @code{proof-goals-font-lock-keywords} and @code{proof-response-font-lock-keywords}. @end defvar @c TEXI DOCSTRING MAGIC: proof-goals-font-lock-keywords @defvar proof-goals-font-lock-keywords -Value of @samp{@code{font-lock-keywords}} used to fontify the goals output.@* -The goals shell mode should set this before calling @samp{@code{proof-goals-config-done}}. -Used also by @samp{@code{proof-easy-config}} mechanism. -See also @samp{@code{proof-script-font-lock-keywords}} and @samp{@code{proof-response-font-lock-keywords}}. +Value of @code{font-lock-keywords} used to fontify the goals output.@* +The goals shell mode should set this before calling @code{proof-goals-config-done}. +Used also by @code{proof-easy-config} mechanism. +See also @code{proof-script-font-lock-keywords} and @code{proof-response-font-lock-keywords}. @end defvar @c TEXI DOCSTRING MAGIC: proof-response-font-lock-keywords @defvar proof-response-font-lock-keywords -Value of @samp{@code{font-lock-keywords}} used to fontify the response output.@* -The response mode should set this before calling @samp{@code{proof-response-config-done}}. -Used also by @samp{@code{proof-easy-config}} mechanism. -See also @samp{@code{proof-script-font-lock-keywords}} and @samp{@code{proof-goals-font-lock-keywords}}. +Value of @code{font-lock-keywords} used to fontify the response output.@* +The response mode should set this before calling @code{proof-response-config-done}. +Used also by @code{proof-easy-config} mechanism. +See also @code{proof-script-font-lock-keywords} and @code{proof-goals-font-lock-keywords}. @end defvar Proof General provides a special function, @code{proof-zap-commas}, for tweaking the font lock behaviour of provers which have declarations of @@ -2597,7 +2597,7 @@ fontifying the output buffers. @c TEXI DOCSTRING MAGIC: proof-zap-commas @defun proof-zap-commas limit Remove the face of all @samp{,} from point to @var{limit}.@* -Meant to be used from @samp{@code{font-lock-keywords}} as a way +Meant to be used from @code{font-lock-keywords} as a way to unfontify commas in declarations and definitions. Useful for provers which have declarations of the form x,y,z:Ty All that can be said for it is that the previous ways of doing @@ -2608,7 +2608,7 @@ this were even more bogus.... @defvar pg-before-fontify-output-hook 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 (@code{point-max}). +the current restriction, and must return the final value of @code{point-max}. [This hook is presently only used by phox-sym-lock]. @end defvar @@ -2896,7 +2896,7 @@ started since then, then there is obviously no proof-tree display. In this case, this variable stays t and the proof-tree display will be started for the next proof. -Controlled by @samp{@code{proof-tree-external-display-toggle}}. +Controlled by @code{proof-tree-external-display-toggle}. @end defvar In Proof General, the code for the external proof-tree display is @@ -2943,18 +2943,18 @@ 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 -@samp{@code{proof-tree-check-proof-finish}} to delay processing the queue region at +see also @code{proof-tree-handle-delayed-output}. Call +@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 @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 been processed. When the proof-tree display is active, this function is called from -@samp{@code{proof-shell-exec-loop}} after the old item has been removed and before -the next item from @samp{@code{proof-action-list}} is sent to the proof assistant. -At this place @samp{@code{proof-action-list}} can be directly manipulated. +@code{proof-shell-exec-loop} after the old item has been removed and before +the next item from @code{proof-action-list} is sent to the proof assistant. +At this place @code{proof-action-list} can be directly manipulated. @end defun @@ -2974,17 +2974,17 @@ 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 @code{proof-tree-urgent-action}. It examines the delayed output in order to take appropriate actions and maintains the internal state. The delayed output to handle is in the region [@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}]. Urgent messages might be before that, following @var{old-proof-marker}, -which contains the position of @samp{@code{proof-marker}}, before the next +which contains the position of @code{proof-marker}, before the next command was sent to the proof assistant. -All other arguments are (former) fields of the @samp{@code{proof-action-list}} +All other arguments are (former) fields of the @code{proof-action-list} entry that is now finally retired. @var{cmd} is the command, @var{flags} are the flags and @var{span} is the span. @end defun @@ -3190,7 +3190,7 @@ Any other %-prefixed character inserts itself. @deffn Macro proof-defshortcut fn string &optional key Define shortcut function @var{fn} to insert @var{string}, optional keydef @var{key}.@* This is intended for defining proof assistant specific functions. -@var{string} is inserted using @samp{@code{proof-insert}}, which see. +@var{string} is inserted using @code{proof-insert}, which see. @var{key} is added onto proof assistant map. @end deffn The function @code{proof-shell-invisible-command} is a useful utility @@ -3202,11 +3202,11 @@ buffer. @c TEXI DOCSTRING MAGIC: proof-shell-invisible-command @defun proof-shell-invisible-command cmd &optional wait invisiblecallback &rest flags Send @var{cmd} to the proof process.@* -The @var{cmd} is @samp{invisible} in the sense that it is not recorded in buffer. +The @var{cmd} is @code{invisible} in the sense that it is not recorded in buffer. @var{cmd} may be a string or a string-yielding expression. -Automatically add @samp{@code{proof-terminal-string}} if necessary, examining -@samp{proof-shell-no-auto-terminate-commands}. +Automatically add @code{proof-terminal-string} if necessary, examining +@code{proof-shell-no-auto-terminate-commands}. By default, let the command be processed asynchronously. But if optional @var{wait} command is non-nil, wait for processing to finish @@ -3216,10 +3216,10 @@ In case @var{cmd} is (or yields) nil, do nothing. @var{invisiblecallback} will be invoked after the command has finished, if it is set. It should probably run the hook variables -@samp{@code{proof-state-change-hook}}. +@code{proof-state-change-hook}. -@var{flags} are additional flags to put onto the @samp{@code{proof-action-list}}. -The flag @code{'invisible} is always added to @var{flags}. +@var{flags} are additional flags to put onto the @code{proof-action-list}. +The flag @code{invisible} is always added to @var{flags}. @end defun There are several handy macros to help you define functions @@ -3229,7 +3229,7 @@ which invoke @code{proof-shell-invisible-command}. @deffn Macro proof-definvisible fn string &optional key Define function @var{fn} to send @var{string} to proof assistant, optional keydef @var{key}.@* This is intended for defining proof assistant specific functions. -@var{string} is sent using @samp{@code{proof-shell-invisible-command}}, which see. +@var{string} is sent using @code{proof-shell-invisible-command}, which see. @var{string} may be a string or a function which returns a string. @var{key} is added onto proof assistant map. @end deffn @@ -3252,7 +3252,7 @@ The @var{body} can contain occurrences of arg. Format @var{string} by replacing quoted chars by escaped version of @var{filename}. %e uses the canonicalized expanded version of filename (including -directory, using @samp{@code{default-directory}} -- see @samp{@code{expand-file-name}}). +directory, using @code{default-directory} -- see @code{expand-file-name}). %r uses the unadjusted (possibly relative) version of @var{filename}. @@ -3264,7 +3264,7 @@ or extension. Using %e can avoid problems with dumb proof assistants who don't understand ~, for example. -For all these cases, the escapes in @samp{@code{proof-shell-filename-escapes}} +For all these cases, the escapes in @code{proof-shell-filename-escapes} are processed. If @var{string} is in fact a function, instead invoke it on @var{filename} and @@ -3367,7 +3367,7 @@ in the @code{proof-assistants} setting. @c TEXI DOCSTRING MAGIC: proof-assistants @defvar proof-assistants Choice of proof assistants to use with Proof General.@* -A list of symbols chosen from: @samp{coq} @samp{easycrypt} @samp{phox} @samp{qrhl} @samp{pgshell} @samp{pgocaml} @samp{pghaskell}. +A list of symbols chosen from: @code{coq} @code{easycrypt} @code{phox} @code{qrhl} @code{pgshell} @code{pgocaml} @code{pghaskell}. If nil, the default will be ALL available proof assistants. Each proof assistant defines its own instance of Proof General, @@ -3430,7 +3430,7 @@ but which the user may require different values of across provers. The function proof-assistant- is also defined, which can be used in the generic portion of Proof General to access the value for the current prover. -Arguments @var{args} are as for @samp{defcustom}, which see. If a :group argument is +Arguments @var{args} are as for @code{defcustom}, which see. If a :group argument is not supplied, the setting will be added to the internal settings for the current prover (named -config). @end deffn @@ -3500,14 +3500,14 @@ interfacing properly with the @code{customize} mechanism. @c TEXI DOCSTRING MAGIC: proof-set-value @defun proof-set-value sym value -Set a customize variable using @samp{@code{set-default}} and a function.@* -We first call @samp{@code{set-default}} to set @var{sym} to @var{value}. +Set a customize variable using @code{set-default} and a function.@* +We first call @code{set-default} to set @var{sym} to @var{value}. Then if there is a function @var{sym} (i.e. with the same name as the variable @var{sym}), it is called to take some dynamic action for the new setting. If there is no function @var{sym}, we try stripping -@samp{@code{proof-assistant-symbol}} and adding "proof-" instead to get +@code{proof-assistant-symbol} and adding "proof-" instead to get a function name. This extends @code{proof-set-value} to work with generic individual settings. @@ -3518,7 +3518,7 @@ approximation we test whether proof-config is fully-loaded yet. @c TEXI DOCSTRING MAGIC: proof-deftoggle @deffn Macro proof-deftoggle var &optional othername Define a function VAR-toggle for toggling a boolean customize setting @var{var}.@* -The toggle function uses @samp{@code{customize-set-variable}} to change the variable. +The toggle function uses @code{customize-set-variable} to change the variable. @var{othername} gives an alternative name than the default -toggle. The name of the defined function is returned. @end deffn @@ -3557,19 +3557,19 @@ The goals buffer. @c TEXI DOCSTRING MAGIC: proof-buffer-type @defvar proof-buffer-type -Symbol for the type of this buffer: @code{'script}, @code{'shell}, @code{'goals}, or @code{'response}. +Symbol for the type of this buffer: @code{script}, @code{shell}, @code{goals}, or @code{response}. @end defvar @c TEXI DOCSTRING MAGIC: proof-included-files-list @defvar proof-included-files-list List of files currently included in proof process.@* This list contains files in canonical truename format -(see @samp{@code{file-truename}}). +(see @code{file-truename}). Whenever a new file is being processed, it gets added to this list -via the @samp{@code{proof-shell-process-file}} configuration settings. +via the @code{proof-shell-process-file} configuration settings. When the prover retracts a file, this list is resynchronised via the -@samp{@code{proof-shell-retract-files-regexp}} and @samp{@code{proof-shell-compute-new-files-list}} +@code{proof-shell-retract-files-regexp} and @code{proof-shell-compute-new-files-list} configuration settings. Only files which have been @strong{fully} processed should be included here. @@ -3594,7 +3594,7 @@ of the proof (starting from 1). @c TEXI DOCSTRING MAGIC: proof-shell-error-or-interrupt-seen @defvar proof-shell-error-or-interrupt-seen Flag indicating that an error or interrupt has just occurred.@* -Set to @code{'error} or @code{'interrupt} if one was observed from the proof +Set to @code{error} or @code{interrupt} if one was observed from the proof assistant during the last group of commands. @end defvar @@ -3691,22 +3691,22 @@ The current buffer is prepared for scripting. No changes are necessary if it is already in Scripting minor mode. Otherwise, it will become the new active scripting buffer, provided scripting can be switched off in the previous active scripting buffer with -@samp{@code{proof-deactivate-scripting}}. +@code{proof-deactivate-scripting}. Activating a new script buffer is a good time to ask if the user wants to save some buffers; this is done if the user option -@samp{@code{proof-query-file-save-when-activating-scripting}} is set and +@code{proof-query-file-save-when-activating-scripting} is set and provided the optional argument @var{nosaves} is non-nil. The optional argument @var{queuemode} relaxes the test for a busy proof shell to allow one which has mode @var{queuemode}. In all other cases, a proof shell busy error is given. -Finally, the hooks @samp{@code{proof-activate-scripting-hook}} are run. This can +Finally, the hooks @code{proof-activate-scripting-hook} are run. This can be a useful place to configure the proof assistant for scripting in a particular file, for example, loading the correct theory, or whatever. If the hooks issue commands to the proof assistant (via -@samp{@code{proof-shell-invisible-command}}) which result in an error, the +@code{proof-shell-invisible-command}) which result in an error, the activation is considered to have failed and an error is given. @end deffn @@ -3714,7 +3714,7 @@ activation is considered to have failed and an error is given. @deffn Command proof-deactivate-scripting &optional forcedaction Try to deactivate scripting for the active scripting buffer. -Aims to set @samp{@code{proof-script-buffer}} to nil and turn off the +Aims to set @code{proof-script-buffer} to nil and turn off the modeline indicator. No action is required there is no active scripting buffer. @@ -3722,17 +3722,17 @@ We make sure that the active scripting buffer either has no locked region or a full locked region (everything in it has been processed). If this is not already the case, we question the user whether to retract or assert, or automatically take the action indicated in the -user option @samp{@code{proof-auto-action-when-deactivating-scripting}}. +user option @code{proof-auto-action-when-deactivating-scripting}. -If @samp{@code{proof-no-fully-processed-buffer}} is t there is only the choice +If @code{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 @samp{@code{proof-auto-action-when-deactivating-scripting}} to @code{'process} +Setting @code{proof-auto-action-when-deactivating-scripting} to @code{process} is ignored in this case. If the scripting buffer is (or has become) fully processed, and it is associated with a file, it is registered on -@samp{@code{proof-included-files-list}}. Conversely, if it is (or has become) +@code{proof-included-files-list}. Conversely, if it is (or has become) empty, we make sure that it is @strong{not} registered. This is to be certain that the included files list behaves as we might expect with respect to the active scripting buffer, in an attempt to harmonize @@ -3741,12 +3741,12 @@ mixed scripting and file reading in the prover. This function either succeeds, fails because the user refused to process or retract a partly finished buffer, or gives an error message because retraction or processing failed. If this function succeeds, -then @samp{@code{proof-script-buffer}} is nil afterwards. +then @code{proof-script-buffer} is nil afterwards. The optional argument @var{forcedaction} overrides the user option -@samp{@code{proof-auto-action-when-deactivating-scripting}} and prevents +@code{proof-auto-action-when-deactivating-scripting} and prevents questioning the user. It is used to make a value for -the @samp{@code{kill-buffer-hook}} for scripting buffers, so that when +the @code{kill-buffer-hook} for scripting buffers, so that when a scripting buffer is killed it is always retracted. @end deffn @@ -3769,26 +3769,26 @@ a series of commands to be sent to the proof assistant. @c TEXI DOCSTRING MAGIC: proof-script-generic-parse-cmdend @defun proof-script-generic-parse-cmdend -For @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-command-end-regexp}} set. +For @code{proof-script-parse-function} if @code{proof-script-command-end-regexp} set. @end defun @c TEXI DOCSTRING MAGIC: proof-script-generic-parse-cmdstart @defun proof-script-generic-parse-cmdstart -For @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-command-start-regexp}} is set. +For @code{proof-script-parse-function} if @code{proof-script-command-start-regexp} is set. @end defun @c TEXI DOCSTRING MAGIC: proof-script-generic-parse-sexp @defun proof-script-generic-parse-sexp -Used for @samp{@code{proof-script-parse-function}} if @samp{@code{proof-script-sexp-commands}} is set. +Used for @code{proof-script-parse-function} if @code{proof-script-sexp-commands} is set. @end defun @c TEXI DOCSTRING MAGIC: proof-semis-to-vanillas @defun proof-semis-to-vanillas semis &optional queueflags Create vanilla spans for @var{semis} and a list for the queue.@* Proof terminator positions @var{semis} has the form returned by -the function @samp{proof-segment-up-to}. The argument list is destroyed. -The callback in each queue element is @samp{@code{proof-done-advancing}}. +the function @code{proof-segment-up-to}. The argument list is destroyed. +The callback in each queue element is @code{proof-done-advancing}. -If the variable @samp{@code{proof-script-preprocess}} is set (to the name of +If the variable @code{proof-script-preprocess} is set (to the name of a function), call that function to construct the first element of each queue item. @@ -3816,16 +3816,16 @@ The main command for retracting parts of a script is Set up the proof process for retracting until point.@* This calculates the commands to undo to the current point within the locked region. If invoked outside the locked region, undo -the last successfully processed command. See @samp{@code{proof-retract-target}}. +the last successfully processed command. See @code{proof-retract-target}. After retraction has succeeded in the prover, the filter will call -@samp{@code{proof-done-retracting}}. If @var{undo-action} is non-nil, it will +@code{proof-done-retracting}. If @var{undo-action} is non-nil, it will then be invoked on the region in the proof script corresponding to the proof command sequence. -@var{displayflags} control output shown to user, see @samp{@code{proof-action-list}}. +@var{displayflags} control output shown to user, see @code{proof-action-list}. Before the retraction is calculated, we enforce the file-level -protocol with @samp{@code{proof-activate-scripting}}. This has a couple +protocol with @code{proof-activate-scripting}. This has a couple of effects: 1. If the file is completely processed, we have to re-open it @@ -3849,17 +3849,17 @@ proof assistant exits, we use the functions @c TEXI DOCSTRING MAGIC: proof-restart-buffers @defun proof-restart-buffers buffers -Remove all extents in @var{buffers} and maybe reset @samp{@code{proof-script-buffer}}.@* +Remove all extents in @var{buffers} and maybe reset @code{proof-script-buffer}.@* The high-level effect is that all members of @var{buffers} are completely unlocked, including all the necessary cleanup. No effect on a buffer which is nil or killed. If one of the buffers -is the current scripting buffer, then @samp{@code{proof-script-buffer}} will +is the current scripting buffer, then @code{proof-script-buffer} will deactivated. @end defun @c TEXI DOCSTRING MAGIC: proof-script-remove-all-spans-and-deactivate @defun proof-script-remove-all-spans-and-deactivate -Remove all spans from scripting buffers via @samp{@code{proof-restart-buffers}}. +Remove all spans from scripting buffers via @code{proof-restart-buffers}. @end defun @@ -3904,14 +3904,14 @@ 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 @code{'advancing} or @code{'retracting} to +this will be set to the queue mode @code{advancing} or @code{retracting} to indicate the direction of movement. -When this is non-nil, @samp{@code{proof-shell-ready-prover}} will give +When this is non-nil, @code{proof-shell-ready-prover} will give an error if called with a different requested queue mode. -See also functions @samp{@code{proof-activate-scripting}} and -@samp{@code{proof-shell-available-p}}. +See also functions @code{proof-activate-scripting} and +@code{proof-shell-available-p}. @end defvar @c TEXI DOCSTRING MAGIC: proof-marker @@ -3941,43 +3941,43 @@ is a space. @var{action} is the callback to be invoked when this item has been processed by the prover. For normal scripting items it is -@samp{@code{proof-done-advancing}}, for retract items -@samp{@code{proof-done-retracting}}, but there are more possibilities (e.g. -@samp{@code{proof-done-invisible}}, @samp{@code{proof-shell-set-silent}}, -@samp{@code{proof-shell-clear-silent}} and @samp{@code{proof-tree-show-goal-callback}}). +@code{proof-done-advancing}, for retract items +@code{proof-done-retracting}, but there are more possibilities (e.g. +@code{proof-done-invisible}, @code{proof-shell-set-silent}, +@code{proof-shell-clear-silent} and @code{proof-tree-show-goal-callback}). The @var{displayflags} are set for non-scripting commands or for when scripting should not bother the user. They may include @lisp - @code{'invisible} non-script command (@samp{@code{proof-shell-invisible-command}}) - @code{'no-response-display} do not display messages in @strong{response} buffer - @code{'no-error-display} do not display errors/take error action - @code{'no-goals-display} do not goals in @strong{goals} buffer - @code{'keep-response} do not erase the response buffer when goals are shown - @code{'proof-tree-show-subgoal} item inserted by the proof-tree package to display + @code{invisible} non-script command (@code{proof-shell-invisible-command}) + @code{no-response-display} do not display messages in @strong{response} buffer + @code{no-error-display} do not display errors/take error action + @code{no-goals-display} do not goals in @strong{goals} buffer + @code{keep-response} do not erase the response buffer when goals are shown + @code{proof-tree-show-subgoal} item inserted by the proof-tree package to display the current or some other goal - @code{'proof-tree-last-item} marks the item that follows the last show-goal + @code{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 - @code{'priority-action} item added via @code{proof-add-to-priority-queue} - @code{'empty-action-list} @code{proof-shell-empty-action-list-command} should not be + @code{priority-action} item added via proof-add-to-priority-queue + @code{empty-action-list} proof-shell-empty-action-list-command should not be called if this is the last item in the action list - @code{'dont-show-when-silent} Used for commands that should not be followed by a + @code{dont-show-when-silent} Used for commands that should not be followed by a show command when running silent. @end lisp -Note that @code{'invisible} does not imply any of the others. If flags +Note that @code{invisible} does not imply any of the others. If flags 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}}. +See the functions @code{proof-start-queue} and @code{proof-shell-exec-loop}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-old-proof-marker-position @defvar proof-shell-old-proof-marker-position Position of end of second last input inside delayed callbacks.@* -When callbacks of action items are processed, @samp{@code{proof-marker}} has already +When callbacks of action items are processed, @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 callback to access the end of the input belonging to its action-list @@ -4000,17 +4000,17 @@ until the asynchronous background compilation finishes. @c TEXI DOCSTRING MAGIC: proof-second-action-list-active @defvar proof-second-action-list-active -Signals that some items are waiting outside of @samp{@code{proof-action-list}}.@* +Signals that some items are waiting outside of @code{proof-action-list}.@* If this is t it means that some items from the queue region are waiting for being processed in a place different from -@samp{@code{proof-action-list}}. In this case Proof General must behave as if -@samp{@code{proof-action-list}} would be non-empty, when it is, in fact, empty. +@code{proof-action-list}. In this case Proof General must behave as if +@code{proof-action-list} would be non-empty, when it is, in fact, empty. This is used, for instance, for parallel background compilation for Coq: The Require command and the following items are not put -into @samp{@code{proof-action-list}} and are stored somewhere else until the +into @code{proof-action-list} and are stored somewhere else until the background compilation finishes. Then those items are put into -@samp{@code{proof-action-list}} for getting processed. +@code{proof-action-list} for getting processed. @end defvar @c TEXI DOCSTRING MAGIC: pg-subterm-anns-use-stack @@ -4033,7 +4033,7 @@ Does nothing if proof assistant is already running. Also generates goal and response buffers. -If @samp{@code{proof-prog-name-ask}} is set, query the user for the +If @code{proof-prog-name-ask} is set, query the user for the process command. @end deffn @@ -4049,32 +4049,32 @@ restarting the process. @defun proof-shell-kill-function Function run when a proof-shell buffer is killed.@* Try to shut down the proof process nicely and clear locked -regions and state variables. Value for @samp{@code{kill-buffer-hook}} in -shell buffer, called by @samp{@code{proof-shell-bail-out}} if process exits. +regions and state variables. Value for @code{kill-buffer-hook} in +shell buffer, called by @code{proof-shell-bail-out} if process exits. @end defun @c TEXI DOCSTRING MAGIC: proof-shell-exit @deffn Command proof-shell-exit &optional dont-ask Query the user and exit the proof process. -This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function +This simply kills the @code{proof-shell-buffer} relying on the hook function -@samp{@code{proof-shell-kill-function}} to do the hard work. If optional +@code{proof-shell-kill-function} to do the hard work. If optional argument @var{dont-ask} is non-nil, the proof process is terminated without confirmation. The kill function uses @samp{-quit-timeout} as a timeout to wait -after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process. +after sending @code{proof-shell-quit-cmd} before rudely killing the process. This function should not be called if -@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of -@samp{@code{proof-shell-kill-function}} will give strange errors. +@code{proof-shell-exit-in-progress} is t, because a recursive call of +@code{proof-shell-kill-function} will give strange errors. @end deffn @c TEXI DOCSTRING MAGIC: proof-shell-bail-out @defun proof-shell-bail-out process event Value for the process sentinel for the proof assistant @var{process}.@* -If the proof assistant dies, run @samp{@code{proof-shell-kill-function}} to +If the proof assistant dies, run @code{proof-shell-kill-function} to cleanup and remove the associated buffers. The shell buffer is left around so the user may discover what killed the process. @var{event} is the string describing the change. @@ -4082,12 +4082,12 @@ left around so the user may discover what killed the process. @c TEXI DOCSTRING MAGIC: proof-shell-restart @deffn Command proof-shell-restart -Clear script buffers and send @samp{@code{proof-shell-restart-cmd}}.@* +Clear script buffers and send @code{proof-shell-restart-cmd}.@* All locked regions are cleared and the active scripting buffer deactivated. If the proof shell is busy, an interrupt is sent with -@samp{@code{proof-interrupt-process}} and we wait until the process is ready. +@code{proof-interrupt-process} and we wait until the process is ready. The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant @@ -4113,7 +4113,7 @@ functions @code{proof-extend-queue} and @code{proof-shell-exec-loop}. Extend the current queue with @var{queueitems}, queue end @var{end}.@* To make sense, the commands should correspond to processing actions for processing a region from (buffer-queue-or-locked-end) to @var{end}. -The queue mode is set to @code{'advancing} +The queue mode is set to @code{advancing} @end defun @c TEXI DOCSTRING MAGIC: proof-extend-queue @@ -4121,16 +4121,16 @@ The queue mode is set to @code{'advancing} Extend the current queue with @var{queueitems}, queue end @var{end}.@* To make sense, the commands should correspond to processing actions for processing a region from (buffer-queue-or-locked-end) to @var{end}. -The queue mode is set to @code{'advancing} +The queue mode is set to @code{advancing} @end defun @vindex proof-action-list @c TEXI DOCSTRING MAGIC: proof-shell-exec-loop @defun proof-shell-exec-loop -Main loop processing the @samp{@code{proof-action-list}}, called from shell filter. +Main loop processing the @code{proof-action-list}, called from shell filter. -@samp{@code{proof-action-list}} contains a list of (@var{span} @var{command} @var{action} [FLAGS]) lists. +@code{proof-action-list} contains a list of (@var{span} @var{command} @var{action} [FLAGS]) lists. -If this function is called with a non-empty @samp{@code{proof-action-list}}, the +If this function is called with a non-empty @code{proof-action-list}, the head of the list is the previously executed command which succeeded. We execute the callback (@var{action} @var{span}) on the first item, then (@var{action} @var{span}) on any following items which have null as @@ -4150,7 +4150,7 @@ by the low-level function @code{proof-shell-insert}. @c TEXI DOCSTRING MAGIC: proof-shell-insert @defun proof-shell-insert strings action &optional scriptspan -Insert @var{strings} at the end of the proof shell, call @samp{@code{scomint-send-input}}. +Insert @var{strings} at the end of the proof shell, call @code{scomint-send-input}. @var{strings} is a list of strings (which will be concatenated), or a single string. @@ -4158,7 +4158,7 @@ single string. The @var{action} argument is a symbol which is typically the name of a callback for when each string has been processed. -This calls @samp{@code{proof-shell-insert-hook}}. The arguments @var{action} and +This calls @code{proof-shell-insert-hook}. The arguments @var{action} and @var{scriptspan} may be examined by the hook to determine how to modify the string variable (exploiting dynamic scoping) which will be the command actually sent to the shell. @@ -4167,12 +4167,12 @@ Note that the hook is not called for the empty (null) string or a carriage return. We strip the string of carriage returns before inserting it -and updating @samp{@code{proof-marker}} to point to the end of the newly +and updating @code{proof-marker} to point to the end of the newly inserted text. Do not use this function directly, or output will be lost. It is only -used in @samp{@code{proof-add-to-queue}} when we start processing a queue, and in -@samp{@code{proof-shell-exec-loop}}, to process the next item. +used in @code{proof-add-to-queue} when we start processing a queue, and in +@code{proof-shell-exec-loop}, to process the next item. @end defun @@ -4184,13 +4184,13 @@ not need to use these directly. @c TEXI DOCSTRING MAGIC: proof-grab-lock @defun proof-grab-lock &optional queuemode Grab the proof shell lock, starting the proof assistant if need be.@* -Runs @samp{@code{proof-state-change-hook}} to notify state change. +Runs @code{proof-state-change-hook} to notify state change. If @var{queuemode} is supplied, set the lock to that value. @end defun @c TEXI DOCSTRING MAGIC: proof-release-lock @defun proof-release-lock -Release the proof shell lock. Clear @samp{@code{proof-shell-busy}}. +Release the proof shell lock. Clear @code{proof-shell-busy}. @end defun @@ -4234,7 +4234,7 @@ if you don't need it (slight speed penalty). @c TEXI DOCSTRING MAGIC: proof-shell-last-prompt @defvar proof-shell-last-prompt A raw record of the last prompt seen from the proof system.@* -This is the string matched by @samp{@code{proof-shell-annotated-prompt-regexp}}. +This is the string matched by @code{proof-shell-annotated-prompt-regexp}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-last-output @@ -4248,21 +4248,21 @@ This is raw string, for internal use only. A symbol denoting the type of the last output string from the proof system.@* Specifically: @lisp - @code{'interrupt} An interrupt message - @code{'error} An error message - @code{'loopback} A command sent from the PA to be inserted into the script - @code{'response} A response message - @code{'goals} A goals (proof state) display - @code{'systemspecific} Something specific to a particular system, - -- see @samp{@code{proof-shell-handle-output-system-specific}} + @code{interrupt} An interrupt message + @code{error} An error message + @code{loopback} A command sent from the PA to be inserted into the script + @code{response} A response message + @code{goals} A goals (proof state) display + @code{systemspecific} Something specific to a particular system, + -- see @code{proof-shell-handle-output-system-specific} @end lisp -The output corresponding to this will be in @samp{@code{proof-shell-last-output}}. +The output corresponding to this will be in @code{proof-shell-last-output}. -See also @samp{@code{proof-shell-proof-completed}} for further information about +See also @code{proof-shell-proof-completed} for further information about the proof process output, when ends of proofs are spotted. This variable can be used for instance specific functions which want -to examine @samp{@code{proof-shell-last-output}}. +to examine @code{proof-shell-last-output}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-last-output-kind @@ -4270,38 +4270,38 @@ to examine @samp{@code{proof-shell-last-output}}. A symbol denoting the type of the last output string from the proof system.@* Specifically: @lisp - @code{'interrupt} An interrupt message - @code{'error} An error message - @code{'loopback} A command sent from the PA to be inserted into the script - @code{'response} A response message - @code{'goals} A goals (proof state) display - @code{'systemspecific} Something specific to a particular system, - -- see @samp{@code{proof-shell-handle-output-system-specific}} + @code{interrupt} An interrupt message + @code{error} An error message + @code{loopback} A command sent from the PA to be inserted into the script + @code{response} A response message + @code{goals} A goals (proof state) display + @code{systemspecific} Something specific to a particular system, + -- see @code{proof-shell-handle-output-system-specific} @end lisp -The output corresponding to this will be in @samp{@code{proof-shell-last-output}}. +The output corresponding to this will be in @code{proof-shell-last-output}. -See also @samp{@code{proof-shell-proof-completed}} for further information about +See also @code{proof-shell-proof-completed} for further information about the proof process output, when ends of proofs are spotted. This variable can be used for instance specific functions which want -to examine @samp{@code{proof-shell-last-output}}. +to examine @code{proof-shell-last-output}. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-start @defvar proof-shell-delayed-output-start 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 -in @samp{@code{proof-shell-filter}}, i.e., when subsequent output arrives. +in @code{proof-shell-filter}, i.e., when subsequent output arrives. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-end @defvar proof-shell-delayed-output-end 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 -in @samp{@code{proof-shell-filter}}, i.e., when subsequent output arrives. +in @code{proof-shell-filter}, i.e., when subsequent output arrives. @end defvar @c TEXI DOCSTRING MAGIC: proof-shell-delayed-output-flags @defvar proof-shell-delayed-output-flags -A copy of the @samp{@code{proof-action-list}} flags for @samp{proof-shell-delayed-output}.@* -Reset in @samp{@code{proof-shell-filter}}, i.e., when subsequent output arrives. +A copy of the @code{proof-action-list} flags for @code{proof-shell-delayed-output}.@* +Reset in @code{proof-shell-filter}, i.e., when subsequent output arrives. @end defvar @vindex proof-action-list @@ -4315,19 +4315,19 @@ goals and loopbacks (proof step hints/proof by pointing results). In this function we check, in turn: @lisp - @samp{@code{proof-shell-interrupt-regexp}} - @samp{@code{proof-shell-error-regexp}} - @samp{@code{proof-shell-proof-completed-regexp}} - @samp{@code{proof-shell-result-start}} + @code{proof-shell-interrupt-regexp} + @code{proof-shell-error-regexp} + @code{proof-shell-proof-completed-regexp} + @code{proof-shell-result-start} @end lisp Other kinds of output are essentially display only, so only dealt with if necessary. -To extend this, set @samp{@code{proof-shell-handle-output-system-specific}}, +To extend this, set @code{proof-shell-handle-output-system-specific}, which is a hook to take particular additional actions. -This function sets variables: @samp{@code{proof-shell-last-output-kind}}, -and the counter @samp{@code{proof-shell-proof-completed}} which counts commands +This function sets variables: @code{proof-shell-last-output-kind}, +and the counter @code{proof-shell-proof-completed} which counts commands after a completed proof. @end defun @@ -4335,25 +4335,25 @@ after a completed proof. @c TEXI DOCSTRING MAGIC: proof-shell-handle-delayed-output @defun proof-shell-handle-delayed-output Display delayed goals/responses, when queue is stopped or completed.@* -This function handles the cases of @samp{proof-shell-output-kind} which +This function handles the cases of @code{proof-shell-output-kind} which are not dealt with eagerly during script processing, namely -@code{'response} and @code{'goals} types. +@code{response} and @code{goals} types. This is useful even with empty delayed output as it will empty the buffers. The delayed output is in the region -[@code{proof-shell-delayed-output-start},@code{proof-shell-delayed-output-end}]. +[@code{proof-shell-delayed-output-start}, @code{proof-shell-delayed-output-end}]. If no goals classified output is found, the whole output is displayed in the response buffer. If goals output is found, the last matching instance, possibly -bounded by @samp{@code{proof-shell-end-goals-regexp}}, will be displayed +bounded by @code{proof-shell-end-goals-regexp}, will be displayed in the goals buffer (and may be further analysed by Proof General). Any output that appears @strong{before} the last goals output (but -after messages classified as urgent, see @samp{@code{proof-shell-filter}}) +after messages classified as urgent, see @code{proof-shell-filter}) will also be displayed in the response buffer. For example, if @var{output} has this form: @@ -4368,18 +4368,18 @@ then @var{goals-2} will be displayed in the goals buffer, and @var{message-2} in the response buffer. @var{junk} will be ignored. Notice that the above alternation (and separation of @var{junk}) can -only be distinguished if both @samp{@code{proof-shell-start-goals-regexp}} -and @samp{@code{proof-shell-end-goals-regexp}} are set. With just the start +only be distinguished if both @code{proof-shell-start-goals-regexp} +and @code{proof-shell-end-goals-regexp} are set. With just the start goals regexp set, @var{goals-2} @var{junk} will appear in the goals buffer and no response output would occur. @lisp @end lisp The goals and response outputs are copied into -@samp{@code{proof-shell-last-goals-output}} and -@samp{@code{proof-shell-last-response-output}} respectively. +@code{proof-shell-last-goals-output} and +@code{proof-shell-last-response-output} respectively. -The value returned is the value for @samp{@code{proof-shell-last-output-kind}}, -i.e., @code{'goals} or @code{'response}. +The value returned is the value for @code{proof-shell-last-output-kind}, +i.e., @code{goals} or @code{response}. @end defun @c TEXI DOCSTRING MAGIC: proof-shell-urgent-message-marker @defvar proof-shell-urgent-message-marker @@ -4397,8 +4397,8 @@ theorem dependency message or interactive output indicator. If none of these apply, display the text between @var{start} and @var{end}. The text between @var{start} and @var{end} should be a string that starts with -text matching @samp{@code{proof-shell-eager-annotation-start}} and -ends with text matching @samp{@code{proof-shell-eager-annotation-end}}. +text matching @code{proof-shell-eager-annotation-start} and +ends with text matching @code{proof-shell-eager-annotation-end}. @end defun The main processing point which triggers other actions is @@ -4411,24 +4411,24 @@ library that is distributed with Proof General (in @c TEXI DOCSTRING MAGIC: proof-shell-filter @defun proof-shell-filter Master filter for the proof assistant shell-process.@* -A function for @samp{@code{scomint-output-filter-functions}}. +A function for @code{scomint-output-filter-functions}. Deal with output and issue new input from the queue. This is an important internal function. The output must be collected from -@samp{@code{proof-shell-buffer}} for the following reason. This function -might block inside @samp{@code{process-send-string}} when sending input to +@code{proof-shell-buffer} for the following reason. This function +might block inside @code{process-send-string} when sending input to the proof assistant or to prooftree. In this case Emacs might call the process filter again while the previous instance is -still running. @samp{@code{proof-shell-filter-wrapper}} detects and delays +still running. @code{proof-shell-filter-wrapper} detects and delays such calls but does not buffer the output. Handle urgent messages first. As many as possible are processed, -using the function @samp{@code{proof-shell-process-urgent-messages}}. +using the function @code{proof-shell-process-urgent-messages}. -If a prompt is seen, run @samp{@code{proof-shell-filter-manage-output}} on the +If a prompt is seen, run @code{proof-shell-filter-manage-output} on the output between the new prompt and the last input (position of -@samp{@code{proof-marker}}) or the last urgent message (position of -@samp{@code{proof-shell-urgent-message-marker}}), whichever is later. For +@code{proof-marker}) or the last urgent message (position of +@code{proof-shell-urgent-message-marker}), whichever is later. For example, in this case: @lisp PROMPT> @var{input} @@ -4439,35 +4439,35 @@ example, in this case: @var{output-3} PROMPT> @end lisp -@samp{@code{proof-marker}} points after @var{input}. +@code{proof-marker} points after @var{input}. -@samp{@code{proof-shell-urgent-message-marker}} points after @var{urgent-message-2}, +@code{proof-shell-urgent-message-marker} points after @var{urgent-message-2}, after both urgent messages have been processed by -@samp{@code{proof-shell-process-urgent-messages}}. Urgent messages always +@code{proof-shell-process-urgent-messages}. Urgent messages always processed; they are intended to correspond to informational notes that the prover makes to inform the user or interface on progress. In this case, the ordinary outputs @var{output-1} and @var{output-2} are ignored; only @var{output-3} will be processed by -@samp{@code{proof-shell-filter-manage-output}}. +@code{proof-shell-filter-manage-output}. Error or interrupt messages are expected to terminate an interactive output and appear last before a prompt and will always be processed. Error messages and interrupt messages are therefore @strong{not} considered as urgent messages. -The first time that a prompt is seen, @samp{@code{proof-marker}} is +The first time that a prompt is seen, @code{proof-marker} is initialised to the end of the prompt. This should correspond -with initializing the process. After that, @samp{@code{proof-marker}} -is only changed when input is sent in @samp{@code{proof-shell-insert}}. +with initializing the process. After that, @code{proof-marker} +is only changed when input is sent in @code{proof-shell-insert}. @end defun @c TEXI DOCSTRING MAGIC: proof-shell-filter-manage-output @defun proof-shell-filter-manage-output start end -Subroutine of @samp{@code{proof-shell-filter}} for output between @var{start} and @var{end}. +Subroutine of @code{proof-shell-filter} for output between @var{start} and @var{end}. -First, we invoke @samp{@code{proof-shell-handle-immediate-output}} which classifies +First, we invoke @code{proof-shell-handle-immediate-output} which classifies and handles output that must be dealt with immediately. Other output (user display) is only displayed when the proof @@ -4480,17 +4480,17 @@ by the filter is to send the next command from the queue. @c TEXI DOCSTRING MAGIC: proof-shell-filter-wrapper @defun proof-shell-filter-wrapper str-do-not-use -Wrapper for @samp{@code{proof-shell-filter}}, protecting against parallel calls.@* +Wrapper for @code{proof-shell-filter}, protecting against parallel calls.@* In Emacs a process filter function can be called while the same filter is currently running for the same process, for instance, when the filter blocks on I/O. This wrapper protects the main -entry point, @samp{@code{proof-shell-filter}} against such parallel, +entry point, @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 -@samp{@code{proof-shell-buffer}} (where it is inserted by -@samp{@code{scomint-output-filter}}), relieving this function from the task +is discarded. @code{proof-shell-filter} collects the output from +@code{proof-shell-buffer} (where it is inserted by +@code{scomint-output-filter}), relieving this function from the task to buffer the output that arrives during parallel, overlapping calls. @end defun @@ -4515,7 +4515,7 @@ configuration variable @code{proof-general-debug}. Non-nil to run Proof General in debug mode.@* This changes some behaviour (e.g. markup stripping) and displays debugging messages in the response buffer. To avoid erasing -messages shortly after they're printed, set @samp{@code{proof-tidy-response}} to nil. +messages shortly after they're printed, set @code{proof-tidy-response} to nil. This is only useful for PG developers. The default value is @code{nil}. diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index ab54d57e9..5c26bf413 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -1425,7 +1425,7 @@ to terminate proof commands. LEGO and Isabelle used a semicolon, @deffn Command proof-goto-end-of-locked &optional switch Jump to the end of the locked region, maybe switching to script buffer.@* If called interactively or @var{switch} is non-nil, switch to script buffer. -If called interactively, a mark is set at the current location with @samp{@code{push-mark}} +If called interactively, a mark is set at the current location with @code{push-mark} @end deffn @c PG4: this is not available at the moment @@ -1580,7 +1580,7 @@ Also handy for proof by pointing, in case the last proof-by-pointing command took the proof in a direction you don't like. Notice that the deleted command is put into the Emacs kill ring, so -you can use the usual @samp{yank} and similar commands to retrieve the +you can use the usual @code{yank} and similar commands to retrieve the deleted text. @end deffn @@ -1588,10 +1588,10 @@ deleted text. @c TEXI DOCSTRING MAGIC: proof-goto-point @deffn Command proof-goto-point &optional raw Assert or retract to the command at current position.@* -Calls @samp{@code{proof-assert-until-point}} or @samp{@code{proof-retract-until-point}} as +Calls @code{proof-assert-until-point} or @code{proof-retract-until-point} as appropriate. With prefix argument @var{raw}, the activation of the omit proofs feature -(@samp{@code{proof-omit-proofs-option}}) is temporarily toggled, +(@code{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. @end deffn @@ -1600,7 +1600,7 @@ or to merely assume them and save time. @deffn Command proof-process-buffer &optional raw Process the current (or script) buffer, and maybe move point to the end.@* With prefix argument @var{raw}, the activation of the omit proofs feature -(@samp{@code{proof-omit-proofs-option}}) is temporarily toggled, +(@code{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. @end deffn @@ -1608,14 +1608,14 @@ or to merely assume them and save time. @c TEXI DOCSTRING MAGIC: proof-retract-buffer @deffn Command proof-retract-buffer &optional called-interactively Retract the current buffer, and maybe move point to the start.@* -Point is only moved according to @samp{@code{proof-follow-mode}}, if +Point is only moved according to @code{proof-follow-mode}, if @var{called-interactively} is non-nil, which is the case for all interactive calls. @end deffn @c TEXI DOCSTRING MAGIC: proof-electric-terminator-toggle @deffn Command proof-electric-terminator-toggle &optional arg -Toggle @samp{@code{proof-electric-terminator-enable}}. With @var{arg}, turn on iff ARG>0.@* +Toggle @code{proof-electric-terminator-enable}. With @var{arg}, turn on iff ARG>0.@* This function simply uses @code{customize-set-variable} to set the variable. @end deffn @@ -1728,7 +1728,7 @@ The user is prompted for an argument. @deffn Command pg-response-clear-displays Clear Proof General response and tracing buffers.@* You can use this command to clear the output from these buffers when -it becomes overly long. Particularly useful when @samp{@code{proof-tidy-response}} +it becomes overly long. Particularly useful when @code{proof-tidy-response} is set to nil, so responses are not cleared automatically. @end deffn @@ -1760,15 +1760,15 @@ If a prefix arg is given and there is a selected region, that is pasted into the command. This is handy for copying terms, etc from the script. -If @samp{@code{proof-strict-state-preserving}} is set, and @samp{@code{proof-state-preserving-p}} +If @code{proof-strict-state-preserving} is set, and @code{proof-state-preserving-p} is configured, then the latter is used as a check that the command will be safe to execute, in other words, that it won't ruin synchronization. If when applied to the command it returns false, then an error message is given. @var{warning}: this command risks spoiling synchronization if the test -@samp{@code{proof-state-preserving-p}} is not configured, if it is -only an approximate test, or if @samp{@code{proof-strict-state-preserving}} +@code{proof-state-preserving-p} is not configured, if it is +only an approximate test, or if @code{proof-strict-state-preserving} is off (nil). @end deffn @@ -1790,7 +1790,7 @@ Does nothing if proof assistant is already running. Also generates goal and response buffers. -If @samp{@code{proof-prog-name-ask}} is set, query the user for the +If @code{proof-prog-name-ask} is set, query the user for the process command. @end deffn @@ -1798,28 +1798,28 @@ process command. @deffn Command proof-shell-exit &optional dont-ask Query the user and exit the proof process. -This simply kills the @samp{@code{proof-shell-buffer}} relying on the hook function +This simply kills the @code{proof-shell-buffer} relying on the hook function -@samp{@code{proof-shell-kill-function}} to do the hard work. If optional +@code{proof-shell-kill-function} to do the hard work. If optional argument @var{dont-ask} is non-nil, the proof process is terminated without confirmation. The kill function uses @samp{-quit-timeout} as a timeout to wait -after sending @samp{@code{proof-shell-quit-cmd}} before rudely killing the process. +after sending @code{proof-shell-quit-cmd} before rudely killing the process. This function should not be called if -@samp{@code{proof-shell-exit-in-progress}} is t, because a recursive call of -@samp{@code{proof-shell-kill-function}} will give strange errors. +@code{proof-shell-exit-in-progress} is t, because a recursive call of +@code{proof-shell-kill-function} will give strange errors. @end deffn @c TEXI DOCSTRING MAGIC: proof-shell-restart @deffn Command proof-shell-restart -Clear script buffers and send @samp{@code{proof-shell-restart-cmd}}.@* +Clear script buffers and send @code{proof-shell-restart-cmd}.@* All locked regions are cleared and the active scripting buffer deactivated. If the proof shell is busy, an interrupt is sent with -@samp{@code{proof-interrupt-process}} and we wait until the process is ready. +@code{proof-interrupt-process} and we wait until the process is ready. The restart command should re-synchronize Proof General with the proof assistant, without actually exiting and restarting the proof assistant @@ -2013,7 +2013,7 @@ Non-nil causes Proof General to record output for all proof commands.@* Proof output is recorded as it occurs interactively; normally if many steps are taken at once, this output is suppressed. If this setting is used to enable it, the proof script can be annotated -with full details. See also @samp{@code{proof-output-tooltips}} to enable +with full details. See also @code{proof-output-tooltips} to enable automatic display of output on mouse hovers. The default value is @code{nil}. @@ -2024,7 +2024,7 @@ The default value is @code{nil}. @defopt proof-strict-read-only 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 @code{'retract} which means +read-only region, except for the special value @code{retract} which means undo first. If nil, Proof General is more relaxed (but may give you a reprimand!). @@ -2084,7 +2084,7 @@ off from the keyboard, you can use the key binding: @c TEXI DOCSTRING MAGIC: proof-autosend-toggle @deffn Command proof-autosend-toggle &optional arg -Toggle @samp{@code{proof-autosend-enable}}. With @var{arg}, turn on iff ARG>0.@* +Toggle @code{proof-autosend-enable}. With @var{arg}, turn on iff ARG>0.@* This function simply uses @code{customize-set-variable} to set the variable. @end deffn @@ -2288,12 +2288,12 @@ 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 proofs closed with a cheating command (see -@samp{@code{proof-omit-cheating-regexp}}), i.e., Admitted for Coq, count as +@code{proof-omit-cheating-regexp}), i.e., Admitted for Coq, count as invalid. This command makes sense for a development process where invalid proofs are permitted and vos compilation and the omit proofs -feature (see @samp{@code{proof-omit-proofs-configured}}) are used to work at +feature (see @code{proof-omit-proofs-configured}) are used to work at the most interesting or challenging point instead of on the first invalid proof. @@ -2302,9 +2302,9 @@ 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 +@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 +output via @code{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 @@ -2313,7 +2313,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 -@code{'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. @@ -2327,7 +2327,7 @@ Annotate failing proofs in current buffer with a "@var{fail}" comment.@* This function modifies the current buffer in place. Use with care! -Similarly to @samp{@code{proof-check-report}}, check all opaque proofs in the +Similarly to @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 "@var{fail}" comments (e.g., from a previous run) are deleted @@ -2338,8 +2338,8 @@ placed at the last or second last statement before the opaque proof. For Coq this corresponds to the proof using and the theorem statement, respectively. In both cases the comment is placed at the right margin of the first line, see -@samp{@code{proof-check-annotate-position}} and -@samp{@code{proof-check-annotate-right-margin}}. +@code{proof-check-annotate-position} and +@code{proof-check-annotate-right-margin}. Interactively, this command does not save the current buffer after placing the annotations. With @var{save-buffer} non-nil, the @@ -2349,7 +2349,7 @@ current buffer is saved if it has been modified. @c TEXI DOCSTRING MAGIC: proof-check-annotate-position @defvar proof-check-annotate-position Line for annotating proofs with "@var{pass}" or "@var{fail}" comments.@* -This option determines the line where @samp{@code{proof-check-annotate}} puts +This option determines the line where @code{proof-check-annotate} puts comments with "@var{pass}" and "@var{fail}". Value `'theoren' uses the first line of the second last statement before the start of the opaque proof, which corresponds to the line containing a Theorem @@ -2362,8 +2362,8 @@ Proof using line for Coq. @defvar proof-check-annotate-right-margin Right margin for "@var{pass}" and "@var{fail}" comments.@* This option determines the right margin to which -@samp{@code{proof-check-annotate}} right-aligns the comments with "@var{pass}" -and "@var{fail}". If nil, the value of @samp{@code{fill-column}} is used. +@code{proof-check-annotate} right-aligns the comments with "@var{pass}" +and "@var{fail}". If nil, the value of @code{fill-column} is used. @end defvar @@ -3117,7 +3117,7 @@ List of identifiers to use for completion for this proof assistant.@* Completion is activated with M-x complete. If this table is empty or needs adjusting, please make changes using -@samp{@code{customize-variable}} and post suggestions at +@code{customize-variable} and post suggestions at https://github.com/ProofGeneral/PG/issues @end defvar @@ -3573,7 +3573,7 @@ shown by default on every launch of Proof General. @c TEXI DOCSTRING MAGIC: proof-splash-enable @defopt proof-splash-enable If non-nil, display a splash screen when Proof General is loaded.@* -See @samp{@code{proof-splash-time}} for configuring the time that the splash +See @code{proof-splash-time} for configuring the time that the splash screen is shown. The default value is @code{t}. @@ -3617,7 +3617,7 @@ screen), you can force a frame to stick to showing the goals or response buffer. This option only takes effect if the frame height is bigger than -4 times @samp{@code{window-min-height}} (i.e., bigger than 16 with default +4 times @code{window-min-height} (i.e., bigger than 16 with default values) because there must be enough space to create 3 windows. The default value is @code{t}. @@ -3634,7 +3634,7 @@ If non-nil, automatically remove windows when they are cleaned.@* 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 @code{'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. @@ -3653,7 +3653,7 @@ example. A convenient way to do this is via the user option Whether response and goals buffers have separate frames.@* If non-nil, Emacs will make separate frames (screen windows) for the goals and response buffers, by altering the Emacs variable -@samp{@code{special-display-regexps}}. +@code{special-display-regexps}. The default value is @code{nil}. @end defopt @@ -3683,13 +3683,13 @@ without adjusting window layout. Refresh the display of windows according to current display mode. For multiple frame mode, this function obeys the setting of -@samp{@code{pg-response-eagerly-raise}}, which see. +@code{pg-response-eagerly-raise}, which see. For single frame mode: - In two panes mode, this uses a canonical layout made by splitting Emacs windows in equal proportions. The splitting is vertical if -Emacs width is smaller than @samp{@code{split-width-threshold}} and +Emacs width is smaller than @code{split-width-threshold} and horizontal otherwise. You can then adjust the proportions by dragging the separating bars. @@ -3706,19 +3706,19 @@ dragging the separating bars. - horizontal: 3 columns mode, one for each buffer (script, goals, response). - By default, the display mode is @code{'smart} which automatically chooses + By default, the display mode is @code{smart} which automatically chooses between these 3 modes by considering the current Emacs frame width: if - it is smaller than @samp{@code{split-width-threshold}} then vertical mode is - chosen, otherwise if it is smaller than 1.5 * @samp{@code{split-width-threshold}} + it is smaller than @code{split-width-threshold} then vertical mode is + chosen, otherwise if it is smaller than 1.5 * @code{split-width-threshold} then hybrid mode is chosen, finally if the frame is larger than 1.5 * - @samp{@code{split-width-threshold}} then the horizontal mode is chosen. + @code{split-width-threshold} then the horizontal mode is chosen. - You can change the value of @samp{@code{split-width-threshold}} at your + You can change the value of @code{split-width-threshold} at your will. If you want to force one of the layouts, you can set variable - @samp{@code{proof-three-window-mode-policy}} to @code{'vertical}, @code{'horizontal} or - @code{'hybrid}. The default value is @code{'smart} which sets the automatic + @code{proof-three-window-mode-policy} to @code{vertical}, @code{horizontal} or + @code{hybrid}. The default value is @code{smart} which sets the automatic behaviour described above. @end lisp @end deffn @@ -3734,7 +3734,7 @@ The default value is @code{nil}. @c TEXI DOCSTRING MAGIC: proof-colour-locked @defopt proof-colour-locked -If non-nil, colour the locked region with @samp{@code{proof-locked-face}}.@* +If non-nil, colour the locked region with @code{proof-locked-face}.@* If this is not set, buffers will have no special face set on locked regions. @@ -3746,7 +3746,7 @@ The default value is @code{t}. Non-nil causes Proof General to add tooltips for prover output.@* Hovers will be added when this option is non-nil. Prover outputs can be displayed when the mouse hovers over the region that -produced it and output is available (see @samp{@code{proof-full-annotation}}). +produced it and output is available (see @code{proof-full-annotation}). If output is not available, the type of the output region is displayed. Changes of this option will not be reflected in already-processed regions of the script. @@ -3791,7 +3791,7 @@ customize to be sure that Proof General reconfigures itself properly. @defopt proof-electric-terminator-enable If non-nil, use electric terminator mode.@* If electric terminator mode is enabled, pressing a terminator will -automatically issue @samp{proof-assert-next-command} for convenience, +automatically issue @code{proof-assert-next-command} for convenience, to send the command straight to the proof process. If the command you want to send already has a terminator character, you don't need to delete the terminator character first. Just press the @@ -3857,8 +3857,8 @@ for the asserted region at the cost of not checking the proofs. For partial and non-opaque proofs in the asserted region all proof commands are sent to the proof assistant. -Using a prefix argument for @samp{@code{proof-goto-point}} (M-x @code{proof-goto-point}) -or @samp{@code{proof-process-buffer}} (M-x @code{proof-process-buffer}) temporarily +Using a prefix argument for @code{proof-goto-point} (M-x proof-goto-point) +or @code{proof-process-buffer} (M-x proof-process-buffer) temporarily disables omitting proofs. @end defvar @@ -3872,9 +3872,9 @@ The default value is @code{nil}. @c TEXI DOCSTRING MAGIC: PA-prog-args @defvar PA-prog-args -Arguments to be passed to @samp{@code{proof-prog-name}} to run the proof assistant.@* -If non-nil, will be treated as a list of arguments for @samp{@code{proof-prog-name}}. -Otherwise @samp{@code{proof-prog-name}} will be split on spaces to form arguments. +Arguments to be passed to @code{proof-prog-name} to run the proof assistant.@* +If non-nil, will be treated as a list of arguments for @code{proof-prog-name}. +Otherwise @code{proof-prog-name} will be split on spaces to form arguments. Remark: Arguments are interpreted strictly: each one must contain only one word, with no space (unless it is the same word). For example if the @@ -3884,18 +3884,18 @@ arguments are -x foo -y bar, then the list should be '("-x" "foo" @c TEXI DOCSTRING MAGIC: PA-prog-env @defvar PA-prog-env -Modifications to @samp{@code{process-environment}} made before running @samp{@code{proof-prog-name}}.@* +Modifications to @code{process-environment} made before running @code{proof-prog-name}.@* Each element should be a string of the form ENVVARNAME=@var{value}. They will be added to the environment before launching the prover (but not pervasively). For example for coq on Windows you might need something like: -(setq @code{coq-prog-env} '("HOME=C:\Program Files\Coq\")) +(setq coq-prog-env '("HOME=C:\Program Files\Coq\")) @end defvar @c TEXI DOCSTRING MAGIC: proof-prog-name-guess @defopt proof-prog-name-guess -If non-nil, use @samp{@code{proof-guess-command-line}} to guess @samp{@code{proof-prog-name}}.@* -This option is compatible with @samp{@code{proof-prog-name-ask}}. -No effect if @samp{@code{proof-guess-command-line}} is nil. +If non-nil, use @code{proof-guess-command-line} to guess @code{proof-prog-name}.@* +This option is compatible with @code{proof-prog-name-ask}. +No effect if @code{proof-guess-command-line} is nil. The default value is @code{nil}. @end defopt @@ -3936,7 +3936,7 @@ The default value is @code{32}. Non-nil to run Proof General in debug mode.@* This changes some behaviour (e.g. markup stripping) and displays debugging messages in the response buffer. To avoid erasing -messages shortly after they're printed, set @samp{@code{proof-tidy-response}} to nil. +messages shortly after they're printed, set @code{proof-tidy-response} to nil. This is only useful for PG developers. The default value is @code{nil}. @@ -3948,24 +3948,24 @@ The default value is @code{nil}. @c TEXI DOCSTRING MAGIC: proof-follow-mode @defopt proof-follow-mode Choice of how point moves with script processing commands.@* -One of the symbols: @code{'locked}, @code{'follow}, @code{'followdown}, @code{'ignore}. +One of the symbols: @code{locked}, @code{follow}, @code{followdown}, @code{ignore}. -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 writable region -If @code{'ignore}, point is never moved after movement commands or on errors. +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 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 -M-x @code{proof-goto-end-of-locked} +If you choose @code{ignore}, you can find the end of the locked using +M-x proof-goto-end-of-locked The default value is @code{locked}. @end defopt @c TEXI DOCSTRING MAGIC: proof-auto-action-when-deactivating-scripting @defopt proof-auto-action-when-deactivating-scripting -If @code{'retract} or @code{'process}, do that when deactivating scripting. +If @code{retract} or @code{process}, do that when deactivating scripting. -With this option set to @code{'retract} or @code{'process}, when scripting +With this option set to @code{retract} or @code{process}, when scripting is turned off in a partly processed buffer, the buffer will be retracted or processed automatically. @@ -3981,9 +3981,9 @@ 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 @code{'process} has then the same effect +no sense. Setting this option to @code{process} has then the same effect as leaving it unset (nil). (This behaviour is controlled by -@samp{@code{proof-no-fully-processed-buffer}}.) +@code{proof-no-fully-processed-buffer}.) The default value is @code{nil}. @end defopt @@ -3996,7 +3996,7 @@ For example, ssh bigjobs @end lisp Would cause Proof General to issue the command @samp{ssh bigjobs coqtop} -to start Coq remotely on our large compute server called @samp{bigjobs}. +to start Coq remotely on our large compute server called @code{bigjobs}. The protocol used should be configured so that no user interaction (passwords, or whatever) is required to get going. For proper @@ -4528,28 +4528,28 @@ Documentation of the user option @code{coq-project-filename}: @defvar coq-project-filename Variable containing the function detecting a project file. -See its default value @samp{@code{coq--default-project-find-file}} for an example. +See its default value @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 nil otherwise. This is used to detect the Coq project file (using -@samp{@code{locate-dominating-file}}). By default we accept _CoqProject and +@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: +@code{coq-project-filename} directly by using: -(setq @code{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"): 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 +options (preferably one per line). If @code{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 +infer the @code{coq-load-path} and the @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 @@ -4569,11 +4569,11 @@ down to ``Coq Use Project File''). @defvar coq-use-project-file If t, when opening a Coq file read the dominating _CoqProject.@* If t, when a Coq file is opened, Proof General will look for a -project file (see @samp{@code{coq-project-filename}}) somewhere in the +project file (see @code{coq-project-filename}) somewhere in the current directory or its parent directories. If there is one, its contents are read and used to determine the arguments that must be given to coqtop. In particular it sets the load -path (including the -R lib options) (see @samp{@code{coq-load-path}}). +path (including the -R lib options) (see @code{coq-load-path}). @end defvar You can also use the .dir-locals.el as above to configure this setting @@ -5025,10 +5025,10 @@ 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: @code{'ask-coq} to confirm saving all -modified Coq buffers, @code{'ask-all} to confirm saving all modified -buffers, @code{'save-coq} to save all modified Coq buffers without -confirmation and @code{'save-all} to save all modified buffers without +This makes four permitted values: @code{ask-coq} to confirm saving all +modified Coq buffers, @code{ask-all} to confirm saving all modified +buffers, @code{save-coq} to save all modified Coq buffers without +confirmation and @code{save-all} to save all modified buffers without confirmation. This option can be set via menu @@ -5048,7 +5048,7 @@ with synchronous job. With this old method Proof General is locked during compilation. If this setting is t, then the new method is used and compilation jobs are dispatched in parallel in the background. The maximal number of parallel compilation jobs -is set with @samp{@code{coq-max-background-compilation-jobs}}. +is set with @code{coq-max-background-compilation-jobs}. This option can be set/reset via menu @samp{Coq -> Auto Compilation -> Compile Parallel In Background}. @@ -5077,38 +5077,38 @@ This option can be set/reset via menu @defvar coq-max-background-compilation-jobs Maximal number of parallel jobs, if parallel compilation is enabled.@* Use the number of available CPU cores if this is set to -@code{'all-cpus}. This variable is the user setting. The value that is -really used is @samp{@code{coq--internal-max-jobs}}. Use @samp{@code{coq-max-jobs-setter}} +@code{all-cpus}. This variable is the user setting. The value that is +really used is @code{coq--internal-max-jobs}. Use @code{coq-max-jobs-setter} or the customization system to change this variable. Otherwise -your change will have no effect, because @samp{@code{coq--internal-max-jobs}} +your change will have no effect, because @code{coq--internal-max-jobs} is not adapted. @end defvar @c TEXI DOCSTRING MAGIC: coq-max-background-second-stage-percentage @defvar coq-max-background-second-stage-percentage -Percentage of @samp{@code{coq-max-background-compilation-jobs}} for the second stage.@* -This setting configures the maximal number of @samp{`-vok}' or vio2vo background +Percentage of @code{coq-max-background-compilation-jobs} for the second stage.@* +This setting configures the maximal number of @samp{@code{-vok}} or vio2vo background jobs running in a second stage as -percentage of @samp{@code{coq-max-background-compilation-jobs}}. +percentage of @code{coq-max-background-compilation-jobs}. For backward compatibility, if this option is not customized, it is initialized from the now deprecated option -@samp{@code{coq-max-background-vio2vo-percentage}}. +@samp{coq-max-background-vio2vo-percentage}. @end defvar @c TEXI DOCSTRING MAGIC: coq-compile-second-stage-delay @defvar coq-compile-second-stage-delay Delay in seconds before starting the second stage compilation.@* -The delay is applied to both @samp{`-vok}' and vio2vo second stages. +The delay is applied to both @samp{@code{-vok}} and vio2vo second stages. For Coq < 8.11 and vio2vo delay helps to avoid running into a -library inconsistency with @code{'quick-and-vio2vo}, see Coq issue +library inconsistency with @code{quick-and-vio2vo}, see Coq issue #@var{5223}. For backward compatibility, if this option is not customized, it is initialized from the now deprecated option -@samp{@code{coq-compile-vio2vo-delay}}. +@samp{coq-compile-vio2vo-delay}. @end defvar Locking ancestors can be disabled with the following option. @@ -5116,7 +5116,7 @@ Locking ancestors can be disabled with the following option. @c TEXI DOCSTRING MAGIC: coq-lock-ancestors @defvar coq-lock-ancestors If non-nil, lock ancestor module files.@* -If external compilation is used (via @samp{@code{coq-compile-command}}) then +If external compilation is used (via @code{coq-compile-command}) then only the direct ancestors are locked. Otherwise all ancestors are locked when the "Require" command is processed. @@ -5155,7 +5155,7 @@ For instance, "make -C %p %o" expands to "make -C bar foo.vo" when module "foo" from directory "bar" is required. After the substitution the command can be changed in the -minibuffer if @samp{@code{coq-confirm-external-compilation}} is t. +minibuffer if @code{coq-confirm-external-compilation} is t. @end defvar @@ -5189,23 +5189,23 @@ forms of include options (@samp{-I} @samp{-Q} and @samp{-R}). An element can be 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}). + logical path @code{path} (@samp{-R dir path}). - A list of the form @samp{(}recnoimport dir path)' (where dir and path are strings) specifying a directory to be recursively - mapped to the logical path @samp{path} (@samp{-Q dir path}), but not + mapped to the logical path @code{path} (@samp{-Q dir path}), but not imported (modules accessible for import with qualified names only). Note that -Q dir "" has a special, nonrecursive meaning. - A list of the form (8.4 only) @samp{(}nonrec dir path)', specifying a - directory to be mapped to the logical path @code{'path'} ('-I dir -as path'). + directory to be mapped to the logical path 'path' ('-I dir -as path'). @end lisp -For convenience the symbol @samp{rec} can be omitted and entries of +For convenience the symbol @code{rec} can be omitted and entries of 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 -directory (see @samp{@code{coq-load-path-include-current}}). +directory (see @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). @@ -5217,7 +5217,7 @@ not the same (-I is for Coq path). If t, let coqdep search the current directory too.@* Should be t for normal users. If t, pass -Q dir "" to coqdep when processing files in directory "dir" in addition to any entries in -@samp{@code{coq-load-path}}. +@code{coq-load-path}. This setting is only relevant with Coq < 8.5. @end defvar @@ -5240,7 +5240,7 @@ 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, -regardless whether @samp{`-quick}' would be used to compile the file +regardless whether @samp{@code{-quick}} would be used to compile the file or not. @end defvar @@ -5625,14 +5625,14 @@ 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}).@* -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 +If t kill Coq when the opam switch changes (requires @code{opam-switch-mode}).@* +When @code{opam-switch-mode} is loaded and the user changes the opam switch +through @code{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. -See https://github.com/ProofGeneral/opam-switch-mode for @samp{opam-switch-mode} +See https://github.com/ProofGeneral/opam-switch-mode for @code{opam-switch-mode} @end defvar @c ================================================================= diff --git a/easycrypt/easycrypt.el b/easycrypt/easycrypt.el index 621805e77..341d9352c 100644 --- a/easycrypt/easycrypt.el +++ b/easycrypt/easycrypt.el @@ -196,7 +196,7 @@ length of the error." (while (proof-looking-at "\\s-") (forward-char 1))) (defun easycrypt-highlight-error () - "Use ‘easycrypt-get-last-error-location’ to know the position of the + "Use `easycrypt-get-last-error-location' to know the position of the error and then highlight in the script buffer." (proof-with-current-buffer-if-exists proof-script-buffer (let ((mtch (easycrypt-get-last-error-location))) diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el index 2fefc0bf9..63c0b9df7 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 c603d1537..41ec5244c 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-pbrpm.el b/generic/pg-pbrpm.el index 9927b0839..6ec57266d 100644 --- a/generic/pg-pbrpm.el +++ b/generic/pg-pbrpm.el @@ -127,7 +127,7 @@ Matches the region to be returned.") (defun pg-pbrpm-analyse-goal-buffer () "Analyse the goal buffer and produce a table to find goals and hypothesis. -It stores, in the variable ‘pg-pbrpm-goal-description’, a list with shape +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: the position of the first char of the goal @@ -332,7 +332,7 @@ The prover command is processed via pg-pbrpm-run-command." (defun pg-pbrpm-run-command (args) "Insert command into the proof queue and then run it. -\(adapted from ‘proof-insert-pbp-command’)" +\(adapted from `proof-insert-pbp-command')" (let* ((command (pop args)) (act (pop args)) (spans (pop args)) (allspan (pop spans))) (if act (setq command (apply act command spans nil))) (if allspan (setq command (concat "(* " (span-string allspan) " *)\n" command "."))) @@ -439,7 +439,7 @@ If no match found, return the empty string." (point)))) (defun pg-pbrpm-process-click (event start end) - "Return the list of infos about the click needed to call ‘generate-menu’. + "Return the list of infos about the click needed to call `generate-menu'. EVENT is an event." (save-excursion (save-window-excursion @@ -539,7 +539,7 @@ The current (standard) selection in the same buffer is also stored." (pg-pbrpm-do-remember-region (car pair) (cdr pair)))))) (defun pg-pbrpm-process-region (span) -"Return the list of infos on the selected region needed to call ‘generate-menu’. +"Return the list of infos on the selected region needed to call `generate-menu'. SPAN is a span covering the selected region." (let ((start (span-start span)) (end (span-end span)) diff --git a/generic/pg-response.el b/generic/pg-response.el index 648ff79eb..e11db9e2f 100644 --- a/generic/pg-response.el +++ b/generic/pg-response.el @@ -95,7 +95,7 @@ ;; (defvar pg-response-special-display-regexp nil - "Regexp for ‘display-buffer-alist’ for multiple frame use. + "Regexp for `display-buffer-alist' for multiple frame use. Internal variable, setting this will have no effect!") (defconst proof-multiframe-parameters @@ -131,10 +131,10 @@ 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." +See `proof-layout-windows' for more details about POLICY." (if (eq policy 'smart) (cond ((>= (frame-width) (* 1.5 split-width-threshold)) 'horizontal) @@ -144,9 +144,9 @@ 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. +See `proof-layout-windows' for more details about POLICY. This function must not be called if the frame has not enough space for 3 windows (see `window-min-height')." @@ -190,7 +190,7 @@ space for 3 windows (see `window-min-height')." (defun proof-display-three-b (&optional policy) "Layout three buffers in a single frame. Only do this if buffers exist. -In this case, call ‘proof-select-three-b’ with argument POLICY. +In this case, call `proof-select-three-b' with argument POLICY. This function must not be called if the frame has not enough space for 3 windows (see `window-min-height')." @@ -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 8e490eb8e..92078f085 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 @@ -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 7cc43f448..44977b3eb 100644 --- a/generic/pg-vars.el +++ b/generic/pg-vars.el @@ -30,13 +30,13 @@ "Symbol for the customization group of user options for the proof assistant. Do not change this variable! It is set automatically by the mode stub defined in proof-site, from the name given in -‘proof-assistant-table’.") +`proof-assistant-table'.") (defvar proof-assistant-internals-cusgrp nil "Symbol for the customization group of PG internal settings. Do not change this variable! It is set automatically by the mode stub defined in proof-site, from the name given in -‘proof-assistant-table’.") +`proof-assistant-table'.") (defvar proof-assistant "" "Name of the proof assistant Proof General is using. @@ -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-autoloads.el b/generic/proof-autoloads.el index 13cac4fa3..63863ccfe 100644 --- a/generic/proof-autoloads.el +++ b/generic/proof-autoloads.el @@ -172,7 +172,7 @@ Commands:\\ Initialise 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’. +If RINGSIZE is omitted or nil, the size defaults to `bufhist-ring-size'. \(fn &optional READWRITE RINGSIZE)" t nil) @@ -894,7 +894,7 @@ No change to current buffer or point. \(fn &optional QUEUEMODE)" nil nil) (autoload 'proof-shell-live-buffer "proof-shell" "\ -Return non-nil if ‘proof-shell-buffer’ is live." nil nil) +Return non-nil if `proof-shell-buffer' is live." nil nil) (autoload 'proof-shell-available-p "proof-shell" "\ Return non-nil if there is a proof shell active and available. @@ -932,7 +932,7 @@ Begin processing a queue of commands. If START is non-nil, START and END are buffer positions in the active scripting buffer for the queue region. -This function calls ‘proof-add-to-queue’ with args QUEUEITEMS and QUEUEMODE. +This function calls `proof-add-to-queue' with args QUEUEITEMS and QUEUEMODE. \(fn START END QUEUEITEMS &optional QUEUEMODE)" nil nil) @@ -1041,7 +1041,7 @@ Make sure the user gets welcomed one way or another." t nil) ;;; Generated autoloads from proof-syntax.el (autoload 'proof-replace-regexp-in-string "proof-syntax" "\ -Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’. +Like `replace-regexp-in-string', but set `case-fold-search' to `proof-case-fold-search'. \(fn REGEXP REP STRING)" nil nil) diff --git a/generic/proof-config.el b/generic/proof-config.el index 591acf769..9ebf7bfd0 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 @@ -416,10 +416,10 @@ It's safe to leave this setting as nil." :group 'proof-script) (defcustom proof-save-with-hole-result 2 - "How to get theorem name after ‘proof-save-with-hole-regexp’ match. + "How to get theorem name after `proof-save-with-hole-regexp' match. String or Int. -If an int N, use ‘match-string’ to get the value of the Nth parenthesis matched. -If a string, use ‘replace-match’. In this case, ‘proof-save-with-hole-regexp’ +If an int N, use `match-string' to get the value of the Nth parenthesis matched. +If a string, use `replace-match'. In this case, `proof-save-with-hole-regexp' should match the entire command." :type '(choice string integer) :group 'proof-script) @@ -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) @@ -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. @@ -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) @@ -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', @@ -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. @@ -1711,7 +1711,7 @@ if you don't need it (slight speed penalty)." :group 'proof-shell) (defcustom proof-shell-extend-queue-hook nil - "Hooks run by ‘proof-extend-queue’ before extending `proof-action-list'. + "Hooks run by `proof-extend-queue' before extending `proof-action-list'. Can be used to run additional actions before items are added to the queue \(such as compiling required modules for Coq) or to modify the items that are going to be added to @@ -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) @@ -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-script.el b/generic/proof-script.el index 133a4f132..b7d456e84 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 4df977868..cf8a2abce 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). @@ -299,7 +299,7 @@ No change to current buffer or point." ;;;###autoload (defun proof-shell-live-buffer () - "Return non-nil if ‘proof-shell-buffer’ is live." + "Return non-nil if `proof-shell-buffer' is live." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) ;; FIXME: Use process-live-p? @@ -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) @@ -1202,7 +1202,7 @@ priority items can be preserved." If START is non-nil, START and END are buffer positions in the active scripting buffer for the queue region. -This function calls ‘proof-add-to-queue’ with args QUEUEITEMS and QUEUEMODE." +This function calls `proof-add-to-queue' with args QUEUEITEMS and QUEUEMODE." (if start (proof-set-queue-endpoints start end)) (proof-add-to-queue queueitems queuemode)) @@ -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,13 +1794,13 @@ 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. 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. @@ -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)) @@ -2003,8 +2003,8 @@ If TIMEOUTSECS is a number, time out after that many seconds." (error "Proof General: quit in proof-shell-wait"))))) (defun proof-done-invisible (span) - "Callback for ‘proof-shell-invisible-command’. -Call ‘proof-state-change-hook’." + "Callback for `proof-shell-invisible-command'. +Call `proof-state-change-hook'." (run-hooks 'proof-state-change-pre-hook) (run-hooks 'proof-state-change-hook)) @@ -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 a85fabd29..c01eb1bfb 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -59,56 +59,56 @@ nil if a region cannot be found." ;; applicable. (defsubst proof-search-forward (string &optional bound noerror count) - "Like ‘search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `search-forward', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (search-forward string bound noerror count))) ;;;###autoload (defun proof-replace-regexp-in-string (regexp rep string) - "Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `replace-regexp-in-string', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string))) (defsubst proof-re-search-forward (regexp &optional bound noerror count) - "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `re-search-forward', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count))) (defsubst proof-re-search-backward (regexp &optional bound noerror count) - "Like ‘re-search-backward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `re-search-backward', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (re-search-backward regexp bound noerror count))) (defsubst proof-re-search-forward-safe (regexp &optional bound noerror count) - "Like ‘re-search-forward’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `re-search-forward', but set `case-fold-search' to `proof-case-fold-search'." (and regexp (let ((case-fold-search proof-case-fold-search)) (re-search-forward regexp bound noerror count)))) (defsubst proof-string-match (regexp string &optional start) - "Like ‘string-match’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `string-match', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (string-match regexp string start))) (defsubst proof-string-match-safe (regexp string &optional start) - "Like ‘string-match’, but return nil if REGEXP or STRING is nil." + "Like `string-match', but return nil if REGEXP or STRING is nil." (if (and regexp string) (proof-string-match regexp string start))) (defsubst proof-stringfn-match (regexp-or-fn string) - "Like ‘proof-string-match’ if first arg is regexp, otherwise call it." + "Like `proof-string-match' if first arg is regexp, otherwise call it." (cond ((stringp regexp-or-fn) (proof-string-match regexp-or-fn string)) ((functionp regexp-or-fn) (funcall regexp-or-fn string)))) (defsubst proof-looking-at (regexp) - "Like ‘looking-at’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." + "Like `looking-at', but set `case-fold-search' to `proof-case-fold-search'." (let ((case-fold-search proof-case-fold-search)) (looking-at regexp))) (defsubst proof-looking-at-safe (regexp) - "Like ‘proof-looking-at’, but return nil if REGEXP is nil." + "Like `proof-looking-at', but return nil if REGEXP is nil." (if regexp (proof-looking-at regexp))) ;; @@ -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 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 b19cf3162..33b59d64e 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) @@ -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)) @@ -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. @@ -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 be8634b49..bba559d62 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 @@ -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/generic/proof-utils.el b/generic/proof-utils.el index 1d05730f3..1789d0bf8 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -64,7 +64,7 @@ ;; (defmacro proof-with-current-buffer-if-exists (buf &rest body) - "Like ‘with-current-buffer’ if BUF exists and is live, otherwise nothing." + "Like `with-current-buffer' if BUF exists and is live, otherwise nothing." `(if (buffer-live-p ,buf) (with-current-buffer ,buf ,@body))) @@ -73,7 +73,7 @@ ;; which work from different PG buffers (goals, response), typically ;; bound to toolbar commands. (defmacro proof-with-script-buffer (&rest body) - "Execute BODY in some script buffer: current buf, else ‘proof-script-buffer’. + "Execute BODY in some script buffer: current buf, else `proof-script-buffer'. Return nil if not a script buffer or if no active scripting buffer." (declare (debug t)) `(cond @@ -253,12 +253,12 @@ Leave point at END." (defun proof-get-window-for-buffer (buffer) "Find a window for BUFFER, display it there, return the window. NB: may change the selected window. This function is a wrapper on -‘display-buffer’. The idea is that if the user has opened and +`display-buffer'. The idea is that if the user has opened and closed some windows we want to preserve the layout by only switching buffer in already pg-associate windows. So if the buffer is not already displayed, we try to reuse an existing associated window, even if in 3-win mode. If no such window -exists, we fall back to ‘display-buffer’ while protecting script +exists, we fall back to `display-buffer' while protecting script buffer to be hidden or split. Experimentally we display a message from time to time advertising @@ -333,7 +333,7 @@ Ensure that point is visible in window." (recenter -1)))))))))) (defun proof-clean-buffer (buffer) - "Erase BUFFER and hide from display if ‘proof-delete-empty-windows’ set. + "Erase BUFFER and hide from display if `proof-delete-empty-windows' set. Auto deletion only affects selected frame. (We assume that the selected frame is the one showing the script buffer.) No effect if buffer is dead." @@ -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 diff --git a/lib/bufhist.el b/lib/bufhist.el index 72a2f318b..213edb2d1 100644 --- a/lib/bufhist.el +++ b/lib/bufhist.el @@ -286,7 +286,7 @@ If N is omitted or nil, move forward by one item." "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’." +If RINGSIZE is omitted or nil, the size defaults to `bufhist-ring-size'." (interactive) (setq bufhist-ring (make-ring (or ringsize bufhist-ring-size))) (setq bufhist-normal-read-only buffer-read-only) diff --git a/lib/local-vars-list.el b/lib/local-vars-list.el index 247250651..d2b5ec8dc 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 b478f3dec..d9eb9f345 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)))) @@ -203,7 +203,7 @@ A span is before PT if it begins before the character before PT." (defun span-property-safe (span name) "Get the property of span SPAN with property name NAME. -Like ‘span-property’, but return nil if SPAN is nil." +Like `span-property', but return nil if SPAN is nil." (and span (span-property span name))) (defun span-set-start (span value) diff --git a/lib/texi-docstring-magic.el b/lib/texi-docstring-magic.el index 11f055f72..90be08c20 100644 --- a/lib/texi-docstring-magic.el +++ b/lib/texi-docstring-magic.el @@ -126,7 +126,18 @@ Compatibility between FSF Emacs and XEmacs." (setq texi-docstring--in-quoted-region nil) (concat "@end lisp\n" line)) line))))) - ;; 2. Pieces of text `stuff' or surrounded in quotes + ;; 2. Symbols like \\+`symbol' are marked up with @code. + ("\\([\\]\\+`\\([^']+\\)'\\)" + t + ,(lambda (docstring) + (concat "@code{" (match-string 2 docstring) "}"))) + ;; 3. Symbols like `symbol' are marked up with @code. This will catch + ;; most simple symbols made of lower-case letters and hyphens. + ("\\(`\\([a-z-]+\\)'\\)" + t + ,(lambda (docstring) + (concat "@code{" (match-string 2 docstring) "}"))) + ;; 3. Pieces of text `stuff' or surrounded in quotes ;; are marked up with @samp. NB: Must be backquote ;; followed by forward quote for this to work. ;; Can't use two forward quotes else problems with @@ -138,23 +149,11 @@ Compatibility between FSF Emacs and XEmacs." t ,(lambda (docstring) (concat "@samp{" (match-string 2 docstring) "}"))) - ;; 3. Words *emphasized* are made @strong{emphasized} + ;; 4. Words *emphasized* are made @strong{emphasized} ("\\(\\*\\(\\w+\\)\\*\\)" t ,(lambda (docstring) (concat "@strong{" (match-string 2 docstring) "}"))) - ;; 4. Words sym-bol which are symbols become @code{sym-bol}. - ;; Must have at least one hyphen to be recognized, - ;; terminated in whitespace, end of line, or punctuation. - ;; Only consider symbols made from word constituents - ;; and hyphen. - ("\\(\\(\\w+-\\(\\w\\|-\\)+\\)\\)\\(\\s)\\|\\s-\\|\\s.\\|$\\)" - ,(lambda (docstring) - (or (boundp (intern (match-string 2 docstring))) - (fboundp (intern (match-string 2 docstring))))) - ,(lambda (docstring) - (concat "@code{" (match-string 2 docstring) "}" - (match-string 4 docstring)))) ;; 5. Upper cased words ARG corresponding to arguments become ;; @var{arg} ;; In fact, include any word so long as it is more than 3 characters @@ -171,20 +170,11 @@ Compatibility between FSF Emacs and XEmacs." ,(lambda (docstring) (concat "@var{" (downcase (match-string 1 docstring)) "}" (match-string 2 docstring)))) - - ;; 6. Words 'sym which are lisp quoted are - ;; marked with @code. - ("\\(\\(\\s-\\|^\\)'\\(\\(\\w\\|-\\)+\\)\\)\\(\\s)\\|\\s-\\|\\s.\\|$\\)" - t - ,(lambda (docstring) - (concat (match-string 2 docstring) - "@code{'" (match-string 3 docstring) "}" - (match-string 5 docstring)))) - ;; 7,8. Clean up for @lisp environments left with spurious newlines + ;; 6,7. Clean up for @lisp environments left with spurious newlines ;; after 1. ("\\(\\(^\\s-*$\\)\n@lisp\\)" t "@lisp") ("\\(\\(^\\s-*$\\)\n@end lisp\\)" t "@end lisp") - ;; 9. Hack to remove @samp{@var{...}} sequences. + ;; 8. Hack to remove @samp{@var{...}} sequences. ;; Changed to just @samp of uppercase. ("\\(@samp{@var{\\([^}]+\\)}}\\)" t diff --git a/lib/unicode-tokens.el b/lib/unicode-tokens.el index b1b3c8ae3..4ec0dd697 100644 --- a/lib/unicode-tokens.el +++ b/lib/unicode-tokens.el @@ -67,7 +67,7 @@ :group 'unicode-tokens-options) (defun unicode-tokens-toggle-add-help-echo () - "Toggle option ‘unicode-tokens-add-help-echo’." + "Toggle option `unicode-tokens-add-help-echo'." (interactive) (customize-set-variable 'unicode-tokens-add-help-echo (not unicode-tokens-add-help-echo)) @@ -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