Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

texinfo manuals: fix obsolete @inforef #725

Merged
merged 1 commit into from
Jan 17, 2024
Merged

texinfo manuals: fix obsolete @inforef #725

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 8 additions & 7 deletions doc/PG-adapting.texi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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

Expand Down
34 changes: 18 additions & 16 deletions doc/ProofGeneral.texi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.

Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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}.
Expand Down Expand Up @@ -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}.



Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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.
Expand All @@ -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
Expand Down Expand Up @@ -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::
Expand All @@ -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
Expand Down Expand Up @@ -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.
Expand Down
Loading