MasterPrinter Struct Reference

Public interface of class 'MasterPrinter'. More...

#include <MasterPrinter.h>

Related Functions
(Note that these are not member functions.)
int	master_printer_deindent (MasterPrinter_ptr self)
	Restore previous level of indentation.
int	master_printer_indent (MasterPrinter_ptr self)
	Pushes the current level of indentation.
int	master_printer_print_node (MasterPrinter_ptr self, node_ptr n, int priority)
	Private interface of class 'MasterPrinter', to be used by printers.
void	MasterPrinter_close_stream (MasterPrinter_ptr self)
	Closes the current stream, if possible or applicable.
MasterPrinter_ptr	MasterPrinter_create (const NuSMVEnv_ptr env)
	The MasterPrinter class constructor.
int	MasterPrinter_flush_stream (MasterPrinter_ptr self)
	Flushes the current stream, if possible or applicable.
StreamType	MasterPrinter_get_stream_type (const MasterPrinter_ptr self)
	Returns the currently set stream type.
const char *	MasterPrinter_get_streamed_string (const MasterPrinter_ptr self)
	Returns the string that has been streamed.
int	MasterPrinter_print_node (MasterPrinter_ptr self, node_ptr n)
	Prints the given node on the stream currently set.
int	MasterPrinter_print_string (MasterPrinter_ptr self, const char *str)
	Prints the given string on the stream currently set.
void	MasterPrinter_reset_stream (MasterPrinter_ptr self, int offs)
	Reset the stream.
void	MasterPrinter_set_stream_type (MasterPrinter_ptr self, StreamType type, const union StreamTypeArg *arg)
	Sets the stream type to be used to produce a printing result.

---

Detailed Description

Public interface of class 'MasterPrinter'.

Author:

Roberto Cavada

Todo:

: Missing description

Definition of the public accessor for class MasterPrinter

---

Friends And Related Function Documentation

int master_printer_deindent

(

MasterPrinter_ptr

self

)

[related]

Restore previous level of indentation.

Restore previous level of indentation. Raises an internal error if an inconsisten internal state is detected.

The internal status of the master printer is changed

See also:

master_printer_indent

int master_printer_indent

(

MasterPrinter_ptr

self

)

[related]

Pushes the current level of indentation.

The internal status of the master printer is changed

See also:

master_printer_deindent

int master_printer_print_node	(	MasterPrinter_ptr	self,
		node_ptr	n,
		int	priority
	)			[related]

Private interface of class 'MasterPrinter', to be used by printers.

Author:

Roberto Cavada

Todo:

: Missing description

Internal version of the method print_node, callable internally and by printers

void MasterPrinter_close_stream

(

MasterPrinter_ptr

self

)

[related]

Closes the current stream, if possible or applicable.

The currently set stream is closed (file) or reset (string) and the stream type is set to be STREAM_TYPE_DEFAULT. IMPORTANT: If the current stream is nusmv_std{out,err} the stream is not closed.

This function is provided to allow the called to forget the set stream after setting it into the master printer.

MasterPrinter_ptr MasterPrinter_create

(

const NuSMVEnv_ptr

env

)

[related]

The MasterPrinter class constructor.

The MasterPrinter class constructor

See also:

MasterPrinter_destroy

int MasterPrinter_flush_stream

(

MasterPrinter_ptr

self

)

[related]

Flushes the current stream, if possible or applicable.

The currently set stream is flushed out (i.e. no unstreamed data remains afterwards.

StreamType MasterPrinter_get_stream_type

(

const MasterPrinter_ptr

self

)

[related]

Returns the currently set stream type.

Returns the currently set stream type

const char * MasterPrinter_get_streamed_string

(

const MasterPrinter_ptr

self

)

[related]

Returns the string that has been streamed.

Returned string belongs to self, DO NOT free it.

Warning: this method can be called only when the current stream type is STREAM_TYPE_STRING.

See also:

master_printer_reset_string_stream

int MasterPrinter_print_node	(	MasterPrinter_ptr	self,
		node_ptr	n
	)			[related]

Prints the given node on the stream currently set.

If the stream is a string stream, the result can be obtained be calling MasterPrinter_get_streamed_string. Returns 0 if an error occurred for some reason.

int MasterPrinter_print_string	(	MasterPrinter_ptr	self,
		const char *	str
	)			[related]

Prints the given string on the stream currently set.

If the stream is a string stream, the result can be obtained be calling MasterPrinter_get_streamed_string. Returns 0 if an error occurred for some reason.

void MasterPrinter_reset_stream	(	MasterPrinter_ptr	self,
		int	offs
	)			[related]

Reset the stream.

Set the indentation offset for this stream. Negative offsets are silently discarded.

void MasterPrinter_set_stream_type	(	MasterPrinter_ptr	self,
		StreamType	type,
		const union StreamTypeArg *	arg
	)			[related]

Sets the stream type to be used to produce a printing result.

When the given type requires an argument (for example, STREAM_TYPE_FILE requires a file), the argument must be passed by using the 'arg' parameter. When not required (for example STREAM_TYPE_STRING), the caller can pass STREAM_TYPE_ARG_UNUSED as argument.

When STREAM_TYPE_FILE is used, the argument must be the handler of an open writable file.

---

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

• NuSMV/code/nusmv/core/node/printers/MasterPrinter.h
• NuSMV/code/nusmv/core/node/printers/MasterPrinter_private.h