diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 8 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 2 |
2 files changed, 9 insertions, 1 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 739a89af4c..c444b5ae05 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -914,6 +914,14 @@ This command turns off the normal displaying. \subsection[\tt Unset Silent.]{\tt Unset Silent.\optindex{Silent}} This command turns the normal display on. +\subsection[\tt Set Search Output Name Only.]{\tt Set Search Output Name Only.\optindex{Search Output Name Only} +\label{Search-Output-Name-Only} +\index{Search Output Name Only mode}} +This command restricts the output of search commands to identifier names; turning it on causes invocations of {\tt Search}, {\tt SearchHead}, {\tt SearchPattern}, {\tt SearchRewrite} etc. to omit types from their output, printing only identifiers. + +\subsection[\tt Unset Search Output Name Only.]{\tt Unset Search Output Name Only.\optindex{Search Output Name Only}} +This command turns type display in search results back on. + \subsection[\tt Set Printing Width {\integer}.]{\tt Set Printing Width {\integer}.\optindex{Printing Width}} \label{SetPrintingWidth} This command sets which left-aligned part of the width of the screen diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8f9ba1ec60..7a1189ee39 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2841,7 +2841,7 @@ Additionally, it prevents a local definition such as {\tt \ident := configurations containing hypotheses of the form {\tt {\ident} = $u$}, or {\tt $u'$ = \ident} with $u'$ not a variable. -The option is off by default. +The option is on by default. \end{Variants} |