StreamMgr Struct Reference

Public interface of class 'StreamMgr'. More...

#include <StreamMgr.h>

Related Functions
(Note that these are not member functions.)
StreamMgr_ptr	StreamMgr_create (void)
	The StreamMgr class constructor.
void	StreamMgr_dec_indent_size (StreamMgr_ptr self)
	Decrements the indentation of the stream manager.
void	StreamMgr_destroy (StreamMgr_ptr self)
	The StreamMgr class destructor.
void	StreamMgr_flush_streams (const StreamMgr_ptr self)
	Prints on the output stream.
OStream_ptr	StreamMgr_get_error_ostream (const StreamMgr_ptr self)
	Getter for the error internal OStream instance.
FILE *	StreamMgr_get_error_stream (const StreamMgr_ptr self)
	Getter for the error stream.
int	StreamMgr_get_indent_size (const StreamMgr_ptr self)
	Returns the indentation of the stream manager.
FILE *	StreamMgr_get_input_stream (const StreamMgr_ptr self)
	Getter for the input stream.
OStream_ptr	StreamMgr_get_output_ostream (const StreamMgr_ptr self)
	Getter for the output internal OStream instance.
FILE *	StreamMgr_get_output_stream (const StreamMgr_ptr self)
	Getter for the output stream.
void	StreamMgr_inc_indent_size (StreamMgr_ptr self)
	Increments the indentation of the stream manager.
void	StreamMgr_nprint_error (const StreamMgr_ptr self, const MasterPrinter_ptr printer, const char *format,...)
	Prints on the error stream.
void	StreamMgr_nprint_output (const StreamMgr_ptr self, const MasterPrinter_ptr printer, const char *format,...)
	Prints on the output stream.
void	StreamMgr_print_error (const StreamMgr_ptr self, const char *format,...)
	Prints on the output stream.
void	StreamMgr_print_output (const StreamMgr_ptr self, const char *format,...)
	Prints on the output stream.
FILE *	StreamMgr_reset_error_stream (StreamMgr_ptr self)
	Set the output stream to NULL.
void	StreamMgr_reset_indent_size (StreamMgr_ptr self)
	Resets the indentation of the stream manager.
FILE *	StreamMgr_reset_output_stream (StreamMgr_ptr self)
	Set the output stream to NULL.
void	StreamMgr_set_error_stream (StreamMgr_ptr self, FILE *err)
	Setter for the error stream.
void	StreamMgr_set_indent_size (StreamMgr_ptr self, int n)
	Sets the indentation of the stream manager.
void	StreamMgr_set_input_stream (StreamMgr_ptr self, FILE *in)
	Setter for the input stream.
void	StreamMgr_set_output_stream (StreamMgr_ptr self, FILE *out)
	Setter for the output stream.

---

Detailed Description

Public interface of class 'StreamMgr'.

Author:

Alessandro Mariotti The stream manager class holds the error, output and input stream and provides some functionalities to print or read from those streams

Definition of the public accessor for class StreamMgr

---

Friends And Related Function Documentation

StreamMgr_ptr StreamMgr_create

(

void

)

[related]

The StreamMgr class constructor.

The StreamMgr class constructor

See also:

StreamMgr_destroy

void StreamMgr_dec_indent_size

(

StreamMgr_ptr

self

)

[related]

Decrements the indentation of the stream manager.

Decrements the indentation of the stream manager

void StreamMgr_destroy

(

StreamMgr_ptr

self

)

[related]

The StreamMgr class destructor.

The StreamMgr class destructor

See also:

StreamMgr_create

void StreamMgr_flush_streams

(

const StreamMgr_ptr

self

)

[related]

Prints on the output stream.

Prints on the output stream. If the stream is NULL, does not print anything

OStream_ptr StreamMgr_get_error_ostream

(

const StreamMgr_ptr

self

)

[related]

Getter for the error internal OStream instance.

Getter for the error internal OStream instance. Should not be changed from the caller

FILE * StreamMgr_get_error_stream

(

const StreamMgr_ptr

self

)

[related]

Getter for the error stream.

Getter for the error stream

int StreamMgr_get_indent_size

(

const StreamMgr_ptr

self

)

[related]

Returns the indentation of the stream manager.

Returns the indentation of the stream manager

FILE * StreamMgr_get_input_stream

(

const StreamMgr_ptr

self

)

[related]

Getter for the input stream.

Getter for the input stream

OStream_ptr StreamMgr_get_output_ostream

(

const StreamMgr_ptr

self

)

[related]

Getter for the output internal OStream instance.

Getter for the output internal OStream instance. Should not be changed from the caller

FILE * StreamMgr_get_output_stream

(

const StreamMgr_ptr

self

)

[related]

Getter for the output stream.

Getter for the output stream

void StreamMgr_inc_indent_size

(

StreamMgr_ptr

self

)

[related]

Increments the indentation of the stream manager.

Increments the indentation of the stream manager

void StreamMgr_nprint_error	(	const StreamMgr_ptr	self,
		const MasterPrinter_ptr	printer,
		const char *	format,
			...
	)			[related]

Prints on the error stream.

Prints on the error stream. If the stream is NULL, does not print anything. This printing routine supports node_ptr's too. Use format 'N' for nodes

void StreamMgr_nprint_output	(	const StreamMgr_ptr	self,
		const MasterPrinter_ptr	printer,
		const char *	format,
			...
	)			[related]

Prints on the output stream.

Prints on the output stream. If the stream is NULL, does not print anything. This printing routine supports node_ptr's too. Use format 'N' for nodes

void StreamMgr_print_error	(	const StreamMgr_ptr	self,
		const char *	format,
			...
	)			[related]

Prints on the output stream.

Prints on the output stream. If the stream is NULL, does not print anything

void StreamMgr_print_output	(	const StreamMgr_ptr	self,
		const char *	format,
			...
	)			[related]

Prints on the output stream.

Prints on the output stream. If the stream is NULL, does not print anything

FILE * StreamMgr_reset_error_stream

(

StreamMgr_ptr

self

)

[related]

Set the output stream to NULL.

Useful for avoiding OStream_set_stream to close the stream. The old stream is returned

void StreamMgr_reset_indent_size

(

StreamMgr_ptr

self

)

[related]

Resets the indentation of the stream manager.

Resets the indentation of the stream manager

FILE * StreamMgr_reset_output_stream

(

StreamMgr_ptr

self

)

[related]

Set the output stream to NULL.

Useful for avoiding OStream_set_stream to close the stream. The old stream is returned

void StreamMgr_set_error_stream	(	StreamMgr_ptr	self,
		FILE *	err
	)			[related]

Setter for the error stream.

Setter for the error stream

void StreamMgr_set_indent_size	(	StreamMgr_ptr	self,
		int	n
	)			[related]

Sets the indentation of the stream manager.

Sets the indentation of the stream manager

void StreamMgr_set_input_stream	(	StreamMgr_ptr	self,
		FILE *	in
	)			[related]

Setter for the input stream.

Setter for the input stream

void StreamMgr_set_output_stream	(	StreamMgr_ptr	self,
		FILE *	out
	)			[related]

Setter for the output stream.

Setter for the output stream

---

The documentation for this struct was generated from the following file:

• NuSMV/code/nusmv/core/utils/StreamMgr.h