From 3e7d32c7c20a30d276701100b1070062dfa74e3a Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 26 Apr 2004 09:03:46 +0000
Subject: Ajout Set Printing Depth et Set Printing Width

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8551 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 doc/RefMan-oth.tex | 36 +++++++++++++++++++++++++++++++-----
 1 file changed, 31 insertions(+), 5 deletions(-)

diff --git a/doc/RefMan-oth.tex b/doc/RefMan-oth.tex
index 47438d9c5..35c55e07b 100644
--- a/doc/RefMan-oth.tex
+++ b/doc/RefMan-oth.tex
@@ -677,7 +677,7 @@ use in a further session. This file can be given as the {\tt
  The state is saved in the current directory (see \pageref{Pwd}).
 \end{Variants}
 
-\section{Miscellaneous}
+\section{Quitting and debugging}
 
 \subsection{\tt Quit.}\comindex{Quit}
 This command permits to quit \Coq.
@@ -716,6 +716,13 @@ go();;
   environment variable \texttt{COQTOP} to the root of your copy of the sources (see section \ref{EnvVariables}).
 \end{Warnings}
 
+\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
+\label{time}
+This command executes the vernac command \textrm{\textsl{command}}
+and display the time needed to execute it.
+
+\section{Controlling display}
+
 \subsection{\tt Set Silent.}
 \comindex{Begin Silent}
 \label{Begin-Silent}
@@ -725,10 +732,29 @@ This command turns off the normal displaying.
 \subsection{\tt Unset Silent.}\comindex{End Silent}
 This command turns the normal display on.
 
-\subsection{\tt Time \textrm{\textsl{command}}.}\comindex{Time}
-\label{time}
-This command executes the vernac command \textrm{\textsl{command}}
-and display the time needed to execute it.
+\subsection{\tt Set Printing Width {\integer}.}\comindex{Set Printing Width}
+This command sets which left-aligned part of the width of the screen
+is used for display. 
+
+\subsection{\tt Unset Printing Width.}\comindex{Unset Printing Width}
+This command resets the width of the screen used for display to its
+default value (which is 78 at the time of writing this documentation).
+
+\subsection{\tt Test Printing Width.}\comindex{Test Printing Width}
+This command displays the current screen width used for display.
+
+\subsection{\tt Set Printing Depth {\integer}.}\comindex{Set Printing Depth}
+This command sets the nesting depth of the formatter used for
+pretty-printing. Beyond this depth, display of subterms is replaced by
+dots. 
+
+\subsection{\tt Unset Printing Depth.}\comindex{Unset Printing Depth}
+This command resets the nesting depth of the formatter used for
+pretty-printing to its default value (at the
+time of writing this documentation, the default value is 50).
+
+\subsection{\tt Test Printing Depth.}\comindex{Test Printing Depth}
+This command displays the current nesting depth used for display.
 
 %\subsection{\tt Explain ...}
 %Not yet documented.
-- 
cgit v1.2.3