<commit_before>\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
\label{Other-commands}}

\section{Displaying}

\subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
This command displays on the screen informations about the declared or
defined object referred by {\qualid}.

\begin{ErrMsgs}
\item {\qualid} \errindex{not a defined object}
\end{ErrMsgs}

\begin{Variants}
\item {\tt Print Term {\qualid}.}
\comindex{Print Term}\\ 
This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a
global constant. 

\item {\tt About {\qualid}.}
\label{About}
\comindex{About}\\ 
This displays various informations about the object denoted by {\qualid}:
its kind (module, constant, assumption, inductive,
constructor, abbreviation\ldots), long name, type, implicit
arguments and argument scopes. It does not print the body of
definitions or proofs.

%\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
%In case \qualid\ denotes an opaque theorem defined in a section,
%it is stored on a special unprintable form and displayed as 
%{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\
%to be computed and displays it.
\end{Variants}

\subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
This command displays informations about the current state of the
environment, including sections and modules.

\begin{Variants}
\item {\tt Inspect \num.}\comindex{Inspect}\\
This command displays the {\num} last objects of the current
environment, including sections and modules.
\item {\tt Print Section {\ident}.}\comindex{Print Section}\\
should correspond to a currently open section, this command
displays the objects defined since the beginning of this section.
% Discontinued
%% \item {\tt Print.}\comindex{Print}\\
%% This command displays the axioms and variables declarations in the
%% environment as well as the constants defined since the last variable
%% was introduced.
\end{Variants}

\section{Requests to the environment}<commit_msg>Added a section in the documentation of Vernacular commands about Set/Unset/Test. It allowed to document the behaviour of Local and Global on Set and Unset.<commit_after>\chapter[Vernacular commands]{Vernacular commands\label{Vernacular-commands}
\label{Other-commands}}

\section{Displaying}

\subsection[\tt Print {\qualid}.]{\tt Print {\qualid}.\comindex{Print}}
This command displays on the screen informations about the declared or
defined object referred by {\qualid}.

\begin{ErrMsgs}
\item {\qualid} \errindex{not a defined object}
\end{ErrMsgs}

\begin{Variants}
\item {\tt Print Term {\qualid}.}
\comindex{Print Term}\\ 
This is a synonym to {\tt Print {\qualid}} when {\qualid} denotes a
global constant. 

\item {\tt About {\qualid}.}
\label{About}
\comindex{About}\\ 
This displays various informations about the object denoted by {\qualid}:
its kind (module, constant, assumption, inductive,
constructor, abbreviation\ldots), long name, type, implicit
arguments and argument scopes. It does not print the body of
definitions or proofs.

%\item {\tt Print Proof {\qualid}.}\comindex{Print Proof}\\
%In case \qualid\ denotes an opaque theorem defined in a section,
%it is stored on a special unprintable form and displayed as 
%{\tt <recipe>}. {\tt Print Proof} forces the printable form of \qualid\
%to be computed and displays it.
\end{Variants}

\subsection[\tt Print All.]{\tt Print All.\comindex{Print All}}
This command displays informations about the current state of the
environment, including sections and modules.

\begin{Variants}
\item {\tt Inspect \num.}\comindex{Inspect}\\
This command displays the {\num} last objects of the current
environment, including sections and modules.
\item {\tt Print Section {\ident}.}\comindex{Print Section}\\
should correspond to a currently open section, this command
displays the objects defined since the beginning of this section.
% Discontinued
%% \item {\tt Print.}\comindex{Print}\\
%% This command displays the axioms and variables declarations in the
%% environment as well as the constants defined since the last variable
%% was introduced.
\end{Variants}

\section{Options and Flags}
\subsection[\tt Set {\rm\sl option} {\rm\sl value}.]{\tt Set {\rm\sl option} {\rm\sl value}.\comindex{Set}}
This command sets {\rm\sl option} to {\rm\sl value}. The original value of
{\rm\sl option} is restored when the current module ends.

\begin{Variants}
\item {\tt Set {\rm\sl flag}.}\\
This command switches {\rm\sl flag} on. The original state of
{\rm\sl flag} is restored when the current module ends.
\item {\tt Local Set {\rm\sl option} {\rm\sl value}.\comindex{Local Set}}
This command sets {\rm\sl option} to {\rm\sl value}. The original value of
{\rm\sl option} is restored when the current \emph{section} ends.
\item {\tt Local Set {\rm\sl flag}.}\\
This command switches {\rm\sl flag} on. The original state of
{\rm\sl flag} is restored when the current \emph{section} ends.
\item {\tt Global Set {\rm\sl option} {\rm\sl value}.\comindex{Global Set}}
This command sets {\rm\sl option} to {\rm\sl value}. The original value of
{\rm\sl option} is \emph{not} restored at the end of the module. Additionally,
if set in a file, {\rm\sl option} is set to {\rm\sl value} when the file is
{\tt Require}-d.
\item {\tt Global Set {\rm\sl flag}.}\\
This command switches {\rm\sl flag} on. The original state of
{\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
if set in a file, {\rm\sl flag} is switched on when the file is
{\tt Require}-d.
\end{Variants}

\subsection[\tt Unset {\rm\sl flag}.]{\tt Unset {\rm\sl flag}.\comindex{Unset}}
This command switches {\rm\sl flag} off. The original state of {\rm\sl flag}
is restored when the current module ends.

\begin{Variants}
\item {\tt Local Unset {\rm\sl flag}.\comindex{Local Unset}}\\
This command switches {\rm\sl flag} off. The original state of {\rm\sl flag}
is restored when the current \emph{section} ends.
\item {\tt Global Unset {\rm\sl flag}.\comindex{Global Unset}}\\
This command switches {\rm\sl flag} off.  The original state of
{\rm\sl flag} is \emph{not} restored at the end of the module. Additionally,
if set in a file, {\rm\sl flag} is switched on when the file is
{\tt Require}-d.
\end{Variants}

\subsection[\tt Test {\rm\sl option}.]{\tt Test {\rm\sl option}.\comindex{Test}}
This command prints the current value of {\rm\sl option}.

\begin{Variants}
\item {\tt Test {\rm\sl flag}.}\\
This command prints whether {\rm\sl flag} is on or off.
\end{Variants}

\section{Requests to the environment}
{'fraction_non_alphanumeric': 0.12323140118667275, 'fraction_numerical': 0.0, 'mean_word_length': 4.148003132341425, 'pattern_counts': {'":': 0, '<': 5, '<?xml version=': 0, '>': 5, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3275580', 'n_tokens_mistral': 1925, 'n_tokens_neox': 1874, 'n_words': 850}