class TEXT_FILE_WRITE
Summary
Basic output facilities to write a named file on the disk.
Note: most features are common with STD_OUTPUT so you can test your
      program first on the screen and then, changing of instance
      (STD_OUTPUT/TEXT_FILE_WRITE), doing the same on a file.
Direct parents
Inherit list: FILE_STREAM, TERMINAL_OUTPUT_STREAM
Class invariant
Overview
Creation features
{ANY}
Features
{ANY}
{FILTER_OUTPUT_STREAM}
{FILTER}
{}
{ANY}
  • path: STRING
    Not Void when connected to the corresponding file on the disk.
  • is_connected: BOOLEAN
    Is this file connected to some file of the operating system?
{}
{ANY}
{}
{STREAM_HANDLER}
{ANY}
{}
{RECYCLING_POOL}
  • recycle
    Do whatever needs to be done to free resources or recycle other objects when recycling this one
{}
  • dispose
    Action to be executed just before garbage collection reclaims an object.
{}
{ANY}
{ANY}
{FILTER}
{ANY}
{}
{ANY}
{ABSTRACT_STRING}
{ANY}
To write a number:
{ANY}
Other features:
{ANY}
{}
{}
{FILTER}
flushed_character_count: INTEGER_64
writable attribute
{ANY}
Note that '%N' is counted as one character even if two bytes are written in the file.
%
character_count: INTEGER_64
effective function
{ANY}
See also flushed_character_count Note that '%N' is counted as one character even if two bytes are written in the file.
%
require
connect_to (new_path: ABSTRACT_STRING)
effective procedure
{ANY}
Truncate file to zero length or create text file for writing.
The stream is positioned at the beginning of the file.
require
  • not is_connected
  • not_malformed_path: not new_path.is_empty
ensure
connect_for_appending_to (new_path: ABSTRACT_STRING)
effective procedure
{ANY}
Open for writing.
The file is created if it does not exist. The stream is positioned at the end of the file.
require ensure
disconnect
effective procedure
{ANY}
Try to disconnect the stream.
Note that it *does not* ensure that the stream will effectively be disconnected (some terminal streams, for instance, are always connected) but the feature can be used to "shake off" filters.
require
    • is_connected
    • can_disconnect
      • is_connected
      • can_disconnect
      • is_connected
      • can_disconnect
ensure
  • not is_filtered
out_in_tagged_out_memory
effective procedure
{ANY}
Append terse printable representation of current object in tagged_out_memory.
require
      • locked: tagged_out_locked
      • locked: tagged_out_locked
      • locked: tagged_out_locked
      • locked: tagged_out_locked
ensure
  • still_locked: tagged_out_locked
  • not_cleared: tagged_out_memory.count >= old tagged_out_memory.count
  • append_only: old tagged_out_memory.twin.is_equal(tagged_out_memory.substring(1, old tagged_out_memory.count))
filtered_put_character (c: CHARACTER)
effective procedure
require
  • is_connected
  • can_put_character(c)
filtered_flush
effective procedure
require
  • is_connected
ensure
filtered_descriptor: INTEGER_32
effective function
Find the descriptor of the terminal stream...
Filters do not have descriptors of their own
require
    • is_connected
    • filtered_has_descriptor
      • is_connected
      • filtered_has_descriptor
      • is_connected
      • filtered_has_descriptor
filtered_has_descriptor: BOOLEAN
is True
constant attribute
True if the underlying terminal stream has a descriptor
require
    • is_connected
      • is_connected
      • is_connected
filtered_stream_pointer: POINTER
effective function
Find the pointer of the terminal stream...
Filters do not have pointers of their own
require
    • is_connected
    • filtered_has_stream_pointer
      • is_connected
      • filtered_has_stream_pointer
      • is_connected
      • filtered_has_stream_pointer
filtered_has_stream_pointer: BOOLEAN
is True
constant attribute
True if the underlying terminal stream has a pointer
require
    • is_connected
      • is_connected
      • is_connected
writable attribute
{}
buffer_position: INTEGER_32
writable attribute
{}
capacity: INTEGER_32
writable attribute
{}
output_stream: POINTER
writable attribute
{}
make
effective procedure
{}
The new created object is not connected.
ensure
write_buffer
effective procedure
{}
text_file_write_open (path_pointer: POINTER): POINTER
{}
text_file_write_append (path_pointer: POINTER): POINTER
{}
io_fclose (stream: POINTER)
{}
path: STRING
writable attribute
{ANY}
Not Void when connected to the corresponding file on the disk.
is_connected: BOOLEAN
effective function
{ANY}
Is this file connected to some file of the operating system?
ensure
  • definition: Result = path /= Void
set_path (new_path: ABSTRACT_STRING)
effective procedure
{}
ensure
  • path.same_as(new_path.out)
descriptor: INTEGER_32
effective function
{ANY}
Some OS-dependent descriptor.
Mainly used by the sequencer library (see READY_CONDITION).
require
has_descriptor: BOOLEAN
effective function
{ANY}
True if that stream can be associated to some OS-meaningful descriptor.
require
can_disconnect: BOOLEAN
deferred function
{ANY}
True if the stream can be safely disconnected (without data loss, etc.)
require
url: URL
frozen
effective function
{ANY}
The URL to this stream as resource
ensure
  • not_void: Result /= Void
  • always_the_same: Result = url
url_memory: URL
writable attribute
{}
new_url: URL
deferred function
{}
ensure
  • Result /= Void
stream_pointer: POINTER
effective function
Some Back-end-dependent pointer (FILE* in C, InputStream or OutputStream in Java)
has_stream_pointer: BOOLEAN
effective function
True if that stream can be associated to some Back-end-meaningful stream pointer.
require
event_exception: EVENT_DESCRIPTOR
effective function
{ANY}
stream_exception: STREAM_EXCEPTION
writable attribute
{}
recycle
effective procedure
Do whatever needs to be done to free resources or recycle other objects when recycling this one
dispose
effective procedure
{}
Action to be executed just before garbage collection reclaims an object.
sequencer_descriptor (file: POINTER): INTEGER_32
{}
can_put_character (c: CHARACTER): BOOLEAN
effective function
{ANY}
put_character (c: CHARACTER)
effective procedure
{ANY}
require
  • is_connected
  • not is_filtered and then can_put_character(c)
flush
effective procedure
{ANY}
Flushes the pipe.
If is_filtered, calls the filter's flush instead.
require
  • is_connected
detach
effective procedure
{ANY}
Shake off the filter.
ensure
  • not is_filtered
writable attribute
The filter that uses this stream as backend
event_can_write: EVENT_DESCRIPTOR
effective function
{ANY}
writable attribute
{}
as_output_stream: OUTPUT_STREAM
effective function
{}
ensure
  • yes_indeed_it_is_the_same_object: Result.to_pointer = to_pointer
is_filtered: BOOLEAN
deferred function
{ANY}
put_natively_stored_string (s: NATIVELY_STORED_STRING)
effective procedure
require
  • s /= Void
put_abstract_string (s: ABSTRACT_STRING)
effective procedure
require
  • s /= Void
put_string (s: ABSTRACT_STRING)
effective procedure
{ANY}
Output s to current output device.
require
put_unicode_string (unicode_string: UNICODE_STRING)
effective procedure
{ANY}
Output the UTF-8 encoding of the unicode_string.
require
put_line (s: ABSTRACT_STRING)
effective procedure
{ANY}
Output the string followed by a '%N'.
%
put_integer (i: INTEGER_64)
frozen
effective procedure
{ANY}
Output i to current output device.
put_integer_format (i: INTEGER_64, s: INTEGER_32)
frozen
effective procedure
{ANY}
Output i to current output device using at most s character.
put_natural_8 (n: NATURAL_8)
frozen
effective procedure
{ANY}
Output n to current output device.
put_natural_8_format (n: NATURAL_8, s: INTEGER_32)
frozen
effective procedure
{ANY}
Output n to current output device using at most s character.
put_natural_16 (n: NATURAL_16)
frozen
effective procedure
{ANY}
Output n to current output device.
put_natural_16_format (n: NATURAL_16, s: INTEGER_32)
frozen
effective procedure
{ANY}
Output n to current output device using at most s character.
put_natural_32 (n: NATURAL_32)
frozen
effective procedure
{ANY}
Output n to current output device.
put_natural_32_format (n: NATURAL_32, s: INTEGER_32)
frozen
effective procedure
{ANY}
Output n to current output device using at most s character.
put_natural_64 (n: NATURAL_64)
frozen
effective procedure
{ANY}
Output n to current output device.
put_natural_64_format (n: NATURAL_64, s: INTEGER_32)
frozen
effective procedure
{ANY}
Output n to current output device using at most s character.
put_real (r: REAL_64)
effective procedure
{ANY}
Output r to current output device.
put_real_format (r: REAL_64, f: INTEGER_32)
effective procedure
{ANY}
Output r with only f digit for the fractional part.
Examples:
   put_real(3.519,2) print "3.51".
require
put_real_scientific (r: REAL_64, f: INTEGER_32)
effective procedure
{ANY}
Output r using the scientific notation with only f digit for the fractional part.
Examples:
   put_real_scientific(3.519,2) print "3.16e+00".
require
put_number (number: NUMBER)
effective procedure
{ANY}
Output the number.
require
put_boolean (b: BOOLEAN)
effective procedure
{ANY}
Output b to current output device according to the Eiffel format.
put_pointer (p: POINTER)
effective procedure
{ANY}
Output a viewable version of p.
put_new_line
effective procedure
{ANY}
Output a newline character.
put_spaces (nb: INTEGER_32)
effective procedure
{ANY}
Output nb spaces character.
require
append_file (file_name: STRING)
effective procedure
{ANY}
require
tmp_file_read: TEXT_FILE_READ
once function
{}
tmp_string: STRING
once function
{}
io_putc (byte: CHARACTER, stream: POINTER)
{}
io_fwrite (buf: NATIVE_ARRAY[CHARACTER], size: INTEGER_32, stream: POINTER): INTEGER_32
{}
io_flush (stream: POINTER)
{}
set_filter (a_filter: FILTER)
effective procedure
Used by the filter itself to get attached
require
  • a_filter /= Void
ensure