From 43285bd9cafedcf274f6f41f6b47fe302aa16b01 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Tue, 16 Jan 2024 22:37:14 +0100 Subject: [PATCH] texinfo manuals: fix obsolete @inforef In most cases, this is a simple replacement, using @pxref in most cases. --- doc/PG-adapting.texi | 15 ++++++++------- doc/ProofGeneral.texi | 34 ++++++++++++++++++---------------- 2 files changed, 26 insertions(+), 23 deletions(-) diff --git a/doc/PG-adapting.texi b/doc/PG-adapting.texi index 26b04d972..8f057a78f 100644 --- a/doc/PG-adapting.texi +++ b/doc/PG-adapting.texi @@ -270,7 +270,7 @@ prototype is about 25 simple settings. For more advanced features you may need (or want) to write some Emacs Lisp. If you're adding new functionality please consider making it generic for different proof assistants, if appropriate. When writing -your modes, please follow the Emacs Lisp conventions, @inforef{Tips, ,Elisp}. +your modes, please follow the Emacs Lisp conventions, @pxref{Tips,,,Elisp}. The configuration variables are declared in the file @file{generic/proof-config.el}. The details in the central part of this @@ -667,7 +667,7 @@ Note that for the generic functions to work properly, it is @strong{essential} that you set the syntax table for your mode properly, so that comments and strings are recognized. See the Emacs documentation to discover how to do this (particularly for the function -@code{modify-syntax-entry}, (@inforef{Syntax Tables, ,Elisp}). +@code{modify-syntax-entry}, (@pxref{Syntax Tables,,,Elisp}). @xref{Proof script mode}, for more details of the parsing functions. @@ -730,7 +730,7 @@ or @samp{@code{proof-script-parse-function}}. The next four settings configure the comment syntax. Notice that to get reliable behaviour of the parsing functions, you may need to modify the syntax table for your prover's mode. -Read the Elisp manual (@inforef{Syntax Tables, ,Elisp}) for details about that. +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 @@ -1148,9 +1148,9 @@ consistency. Portions that can be potentially omitted are called @emph{opaque proofs} in Proof General, because usually only opaque proofs (in the sense of Coq) can be omitted without risking to break the following code. This feature is also -described in the Proof General manual, @inforef{Script processing -commands, ,ProofGeneral} and @inforef{Omitting proofs for speed, -,ProofGeneral}. +described in the Proof General manual, @pxref{Script processing +commands,,,ProofGeneral} and +@pxref{Omitting proofs for speed,,,ProofGeneral}. The omit proofs feature works in a simple, straightforward way: After parsing the asserted region, Proof General uses regular @@ -2519,7 +2519,8 @@ advantage of not requiring the underlying text to be changed to display symbols. Usage of the Unicode Tokens package is described in the Proof General -user manual, @inforef{Unicode support, ,ProofGeneral}. +user manual, @pxref{Unicode symbols and special layout +support,,,ProofGeneral}. @c FIXME TODO: add documentation here to explain config of Unicode Tokens diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index 229617fdf..d3a28b069 100644 --- a/doc/ProofGeneral.texi +++ b/doc/ProofGeneral.texi @@ -743,7 +743,7 @@ of a common interface mechanism. To get more from Proof General and adapt it to your liking, it helps to know a little bit about how Emacs lisp packages can be customized via the Customization mechanism. It's really easy to use. For details, -@pxref{How to customize}. @inforef{Customization, ,emacs}, +@pxref{How to customize}. @xref{Customization,,,emacs}, for documentation in Emacs. To get the absolute most from Proof General, to improve it or to adapt @@ -1622,7 +1622,7 @@ As experienced Emacs users will know, a @i{prefix argument} is a numeric argument supplied by some key sequence typed before a command key sequence. You can supply a specific number by typing @key{Meta} with the digits, or a ``universal'' prefix of @kbd{C-u}. See -@inforef{Arguments, ,emacs} for more details. Several Proof General +@ref{Arguments,,,emacs} for more details. Several Proof General commands, like @code{proof-retract-until-point-interactive}, may accept a @i{prefix argument} to adjust their behaviour somehow. @@ -2927,7 +2927,7 @@ This is an inherent problem with outline because it works by modifying the buffer. If you want to use outline with processed scripts, you can turn off the @code{Strict Read Only} option. -See @inforef{Outline Mode, ,emacs} for more information about outline mode. +See @ref{Outline Mode,,,emacs} for more information about outline mode. @node Support for completion @section Support for completion @@ -3023,7 +3023,7 @@ General doesn't do this automatically. Apart from completion, there are several other operations on tags. One common one is replacing identifiers across all files using @code{tags-query-replace}. For more information on how to use tags, -@inforef{Tags, ,emacs}. +@pxref{xref,,,emacs}. To use tags for completion at the same time as the completion mechanism mentioned already, you can use the command @kbd{M-x add-completions-from-tags-table}. @@ -3379,7 +3379,7 @@ Proof General has been fully loaded. Proof General is fully loaded when you visit a script file for the first time, or if you type @kbd{M-x load-library RET proof RET}. -For more help with customize, see @inforef{Customization, ,emacs}. +For more help with customize, see @ref{Customization,,,emacs}. @@ -4100,7 +4100,7 @@ and a short-cut for enabling three window mode, @cindex file variables A very convenient way to customize file-specific variables is to use -File Variables (@inforef{File Variables, ,emacs}). This feature of +File Variables (@pxref{File Variables,,,emacs}). This feature of Emacs permits to specify values for certain Emacs variables when a file is loaded. File variables and their values are written as a list at the end of @@ -4144,13 +4144,13 @@ And then the right call to make will be done if you use the @kbd{M-x compile} command, and the correct @code{coqtop} will be called by ProofGeneral. Note that the lines are commented in order to be ignored by the proof assistant. It is possible to use this mechanism for all -variables, @inforef{File Variables, ,emacs}. +variables, @pxref{File Variables,,,emacs}. @emph{NOTE:} @code{coq-prog-name} should contain only the @code{coqtop} executable, @emph{not the options}. One can also specify file variables on a per directory basis, -@inforef{Directory Variables, ,emacs}. You can achieve almost the same +@pxref{Directory Variables,,,emacs}. You can achieve almost the same as above for all the files of a directory by storing @lisp @@ -4161,7 +4161,7 @@ as above for all the files of a directory by storing into the file @code{.dir-locals.el} in one of the parent directories. The value in this file must be an alist that maps mode names to alists, where these latter alists map variables to values. You can aso put -arbitrary code in this file @inforef{Directory Variables, ,emacs}. +arbitrary code in this file @pxref{Directory Variables,,,emacs}. @emph{Note:} if you add such content to the @code{.dir-locals.el} file you should restart Emacs or revert your buffer. @@ -4170,7 +4170,7 @@ you should restart Emacs or revert your buffer. @section Using abbreviations A very useful package of Emacs supports automatic expansions of -abbreviations as you type, @inforef{Abbrevs, ,emacs}. +abbreviations as you type, @pxref{Abbrevs,,,emacs}. For example, the proof assistant Coq has many command strings that are long, such as ``reflexivity,'' ``Inductive,'' ``Definition'' and @@ -4314,10 +4314,12 @@ with the option @code{coq-load-path}, but this is not compatible with @code{CoqIde} or @code{coq_makefile}. @emph{NOTE:} the Coq project file cannot define which version of -@code{coqtop} is launched. You need either to launch emacs with the -right executable in the path or use @inforef{File Variables, ,emacs} or -@inforef{Directory Variables, ,emacs}. See @ref{Using file variables} -below. +@code{coqtop} is launched. @xref{Opam-switch-mode support} for how to +switch between different Coq versions. Alternatively, for a fixed +version, you need either to launch emacs with the right executable in +the path or use file variables (@pxref{Using file variables} below or +@pxref{File Variables,,,emacs}) or directory variables, +@pxref{Directory Variables,,,emacs}. @menu * Changing the name of the coq project file:: @@ -4338,7 +4340,7 @@ If you only want to change the name of the Coq project file for one project you can set the option as local file variable, @ref{Using file variables}. This can be done either directly in every file or once for all files of a directory tree with a -@code{.dir-locals.el} file, @inforef{Directory Variables, ,emacs}. +@code{.dir-locals.el} file, @pxref{Directory Variables,,,emacs}. The file @code{.dir-locals.el} should then contain @lisp @@ -4543,7 +4545,7 @@ Output from the compilation is only shown in case of errors. It then appears in the buffer @code{*coq-compile-response*}. One can use @code{C-x `} (bound to @code{next-error}, -@inforef{Compilation Mode,,emacs}) to jump to error locations. +@pxref{Compilation Mode,,,emacs}) to jump to error locations. Sometimes the compilation commands do not produce error messages with location information, then @code{C-x `} does only work in a limited way.