OStream Struct Reference

Public interface of class 'OStream'. More...

#include <OStream.h>

Related Functions
(Note that these are not member functions.)
OStream_ptr	OStream_copy (OStream_ptr self)
	The OStream class copier.
OStream_ptr	OStream_create (FILE *stream)
	The OStream class constructor.
OStream_ptr	OStream_create_file (const char *fname, boolean append)
	The OStream class constructor.
void	OStream_dec_indent_size (OStream_ptr self)
	Decrements the indentation of the ostream.
void	OStream_destroy (OStream_ptr self)
	The OStream class destructor.
void	OStream_destroy_safe (OStream_ptr self)
	The OStream class destructor.
void	OStream_flush (const OStream_ptr self)
	Flushes the ostream.
int	OStream_get_indent_size (const OStream_ptr self)
	Returns the indentation of the ostream.
FILE *	OStream_get_stream (const OStream_ptr self)
	Getter for the internal FILE* instance.
void	OStream_inc_indent_size (OStream_ptr self)
	Increments the indentation of the ostream.
void	OStream_nprintf (const OStream_ptr self, const MasterPrinter_ptr node_printer, const char *format,...)
	Prints the given format string with the given parameters.
void	OStream_nvprintf (const OStream_ptr self, const MasterPrinter_ptr node_printer, const char *format, va_list args)
	Prints the given format string with the given parameters.
void	OStream_printf (const OStream_ptr self, const char *format,...)
	Prints the given format string with the given parameters.
void	OStream_reset_indent_size (OStream_ptr self)
	Resets the indentation of the ostream.
FILE *	OStream_reset_stream (OStream_ptr self)
	Set the stream to NULL.
void	OStream_set_indent_size (OStream_ptr self, int n)
	Sets the indentation of the ostream.
void	OStream_set_split_newline (OStream_ptr self, boolean enabled)
	Enables/disables newline splitting for indentation.
void	OStream_set_stream (OStream_ptr self, FILE *stream)
	Sets the stream on which the OStream prints.
void	OStream_vprintf (const OStream_ptr self, const char *format, va_list args)
	Prints the given format string with the given parameters.

---

Detailed Description

Public interface of class 'OStream'.

Author:

Alessandro Mariotti

Todo:

: Missing description

Definition of the public accessor for class OStream

---

Friends And Related Function Documentation

OStream_ptr OStream_copy

(

OStream_ptr

self

)

[related]

The OStream class copier.

Internal FILE is referenced, the returned copy MUST be destroyed with destroy_safe

See also:

OStream_create

OStream_ptr OStream_create

(

FILE *

stream

)

[related]

The OStream class constructor.

AutomaticStart

The OStream class constructor

See also:

OStream_destroy

OStream_ptr OStream_create_file	(	const char *	fname,
		boolean	append
	)			[related]

The OStream class constructor.

The OStream class constructor. Opens a new FILE* instance from the given filename. If append is false, flag "w" is used, flag "a" is used otherwise

See also:

OStream_destroy

void OStream_dec_indent_size

(

OStream_ptr

self

)

[related]

Decrements the indentation of the ostream.

Decrements the indentation of the ostream

void OStream_destroy

(

OStream_ptr

self

)

[related]

The OStream class destructor.

The OStream class destructor. If the internal FILE* stream is not stdout or stderr, the stream is closed

See also:

OStream_create

void OStream_destroy_safe

(

OStream_ptr

self

)

[related]

The OStream class destructor.

The OStream class destructor. The internal stream is NOT closed

See also:

OStream_create

void OStream_flush

(

const OStream_ptr

self

)

[related]

Flushes the ostream.

Flushes the ostream

int OStream_get_indent_size

(

const OStream_ptr

self

)

[related]

Returns the indentation of the ostream.

Returns the indentation of the ostream

FILE * OStream_get_stream

(

const OStream_ptr

self

)

[related]

Getter for the internal FILE* instance.

Getter for the internal FILE* instance

See also:

OStream_set_stream

void OStream_inc_indent_size

(

OStream_ptr

self

)

[related]

Increments the indentation of the ostream.

Increments the indentation of the ostream

void OStream_nprintf	(	const OStream_ptr	self,
		const MasterPrinter_ptr	node_printer,
		const char *	format,
			...
	)			[related]

Prints the given format string with the given parameters.

Prints the given format string with the given parameters. Supports node printing (using 'N')

void OStream_nvprintf	(	const OStream_ptr	self,
		const MasterPrinter_ptr	node_printer,
		const char *	format,
		va_list	args
	)			[related]

Prints the given format string with the given parameters.

Prints the given format string with the given parameters. Supports node printing (using 'N')

void OStream_printf	(	const OStream_ptr	self,
		const char *	format,
			...
	)			[related]

Prints the given format string with the given parameters.

Prints the given format string with the given parameters

See also:

OStream_nprintf

void OStream_reset_indent_size

(

OStream_ptr

self

)

[related]

Resets the indentation of the ostream.

Resets the indentation of the ostream

FILE * OStream_reset_stream

(

OStream_ptr

self

)

[related]

Set the stream to NULL.

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

void OStream_set_indent_size	(	OStream_ptr	self,
		int	n
	)			[related]

Sets the indentation of the ostream.

Sets the indentation of the ostream

void OStream_set_split_newline	(	OStream_ptr	self,
		boolean	enabled
	)			[related]

Enables/disables newline splitting for indentation.

Enables/disables newline splitting for indentation

void OStream_set_stream	(	OStream_ptr	self,
		FILE *	stream
	)			[related]

Sets the stream on which the OStream prints.

Sets the stream on which the OStream prints

Flushes the current stream. Closes it if it is not stdout or stderr

void OStream_vprintf	(	const OStream_ptr	self,
		const char *	format,
		va_list	args
	)			[related]

Prints the given format string with the given parameters.

Prints the given format string with the given parameters

See also:

OStream_nprintf

---

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

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