diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index d37fc9f3fc..ed54ecb670 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -920,7 +920,7 @@ or the ascii code of the character \verb!"! (i.e. the ascii code \subsection{Displaying informations about scopes} -\subsubsection{\tt Print Visibility} +\subsubsection{\tt Print Visibility\comindex{Print Visibility}} This displays the current stack of notations in scopes and lonely notations that is used to interpret a notation. The top of the stack @@ -937,13 +937,13 @@ notations assuming that {\scope} is pushed on top of the stack. This is useful to know how a subterm locally occurring in the scope of {\scope} is interpreted. -\subsubsection{\tt Print Scope {\scope}} +\subsubsection{\tt Print Scope {\scope}\comindex{Print Scope}} This displays all the notations defined in interpretation scope {\scope}. It also displays the delimiting key if any and the class to which the scope is bound, if any. -\subsubsection{\tt Print Scopes} +\subsubsection{\tt Print Scopes\comindex{Print Scopes}} This displays all the notations, delimiting keys and corresponding class of all the existing interpretation scopes. |