diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-syn.tex | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/doc/refman/RefMan-syn.tex b/doc/refman/RefMan-syn.tex index 37cbd1eac1..aabc8a8995 100644 --- a/doc/refman/RefMan-syn.tex +++ b/doc/refman/RefMan-syn.tex @@ -757,7 +757,8 @@ ways to change the interpretation of subterms are available. \subsubsection{Local opening of an interpretation scope \label{scopechange} \index{\%} -\comindex{Delimit Scope}} +\comindex{Delimit Scope} +\comindex{Undelimit Scope}} It is possible to locally extend the interpretation scope stack using the syntax ({\term})\%{\delimkey} (or simply {\term}\%{\delimkey} @@ -774,6 +775,12 @@ To bind a delimiting key to a scope, use the command \texttt{Delimit Scope} {\scope} \texttt{with} {\ident} \end{quote} +To remove a delimiting key of a scope, use the command + +\begin{quote} +\texttt{Undelimit Scope} {\scope} +\end{quote} + \subsubsection{Binding arguments of a constant to an interpretation scope \comindex{Arguments}} |