DEFINITION MODULE Base10000IOBuffer;  



PROCEDURE SetDelay (count : CARDINAL);
(* set a delay of this many digits before printing starts; default 0. Note that
    the stream is effectively restarted without flushing. *)

PROCEDURE SquirtUnNormalizedBase10000Digit (d : CARDINAL);
(* squirt another unnormalized "digit" on to the stream---may cause arbitrarily
    many normalized digits to be output. *)

PROCEDURE FlushBufferedDigitStream();
(* terminate the stream by flushing any digits still buffered. *)



END (* DEFINITION MODULE *) Base10000IOBuffer.  
