diff options
| author | Pierre Courtieu | 2017-08-16 16:32:44 +0200 |
|---|---|---|
| committer | Pierre Courtieu | 2017-08-17 10:42:03 +0200 |
| commit | 7ca4cd26d67070058589031b693454cd2858e4e9 (patch) | |
| tree | 495fbbdac5c9cfe688ca4bc7edc1b293dac189a2 /doc/refman/RefMan-oth.tex | |
| parent | 16b0b833a3cee070a207e2039bde0ae77b8774d4 (diff) | |
Adding documentation for Printing Focused option.
Diffstat (limited to 'doc/refman/RefMan-oth.tex')
| -rw-r--r-- | doc/refman/RefMan-oth.tex | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index bf48057cdf..8f43ebcfbc 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -974,7 +974,20 @@ line provided it does not exceed the printing width (See {\tt Set Printing Width} above). \subsection[\tt Test Printing Compact Contexts.]{\tt Test Printing Compact Contexts.\optindex{Printing Compact Contexts}} -This command displays the current state of compaction of goal d'isolat. +This command displays the current state of compaction of goal. + + +\subsection[\tt Unset Printing Unfocused.]{\tt Unset Printing Unfocused.\optindex{Printing Unfocused}} +This command resets the displaying of goals to focused goals only +(default). Unfocused goals are created by focusing other goals with +bullets(see~\ref{bullets}) or curly braces (see~\ref{curlybacket}). + +\subsection[\tt Set Printing Unfocused.]{\tt Set Printing Unfocused.\optindex{Printing Unfocused}} +This command enables the displaying of unfocused goals. The goals are +displayed after the focused ones and are distinguished by a separator. + +\subsection[\tt Test Printing Unfocused.]{\tt Test Printing Unfocused.\optindex{Printing Unfocused}} +This command displays the current state of unfocused goals display. \subsection[\tt Set Printing Dependent Evars Line.]{\tt Set Printing Dependent Evars Line.\optindex{Printing Dependent Evars Line}} This command enables the printing of the ``{\tt (dependent evars: \ldots)}'' |