----------------------------------------------------------------------
max_print_depth                                              (Globals)
----------------------------------------------------------------------
max_print_depth : int ref

SYNOPSIS
Sets depth bound on prettyprinting.

DESCRIBE
The reference variable {max_print_depth} is used to define the
maximum depth of printing for the pretty printer. If the number of
blocks (an internal notion used by the prettyprinter) becomes greater
than the value set by {max_print_depth} then the blocks are
abbreviated by the holophrast {...}. By default, the value of
{max_print_depth} is {~1}. This is interpreted to mean ‘print everything’.

FAILURE
Never fails.

EXAMPLE
To change the maximum depth setting to {10}, the command will be:

   - max_print_depth := 10;
   > val it = () : unit

The theorem {numeralTheory.numeral_distrib} then prints as
follows:

- numeralTheory.numeral_distrib;
> val it =
    |- (!n. 0 + n = n) /\ (!n. n + 0 = n) /\
       (!n m. NUMERAL n + NUMERAL m = NUMERAL (iZ (n + m))) /\
       (!n. 0 * n = 0) /\ (!n. n * 0 = 0) /\
       (!n m. ... ... * ... ... = NUMERAL (... * ...)) /\
       (!n. ... - ... = 0) /\ (!n. ... = ...) /\ (!... .... ...) /\ ... /\ ...
     : thm




----------------------------------------------------------------------