Eiffel Media API
Overview Cluster Class Classes Index      Previous Next      Top Features

kernel.spec.ise

Class KL_STDOUT_FILE


Direct ancestors

KI_TEXT_OUTPUT_STREAM, KL_OPERATING_SYSTEM, CONSOLE

Creation

Features

Invariants

indexing

description

Standard output files containing extended ASCII characters %
%(8-bit code between 0 and 255). The character '%N' is automatically %
%converted to the line separtor of the underlying file system when %
%written to the standard output file.

library

Gobo Eiffel Kernel Library

copyright

Copyright (c) 2001, Eric Bezault and others

license

Eiffel Forum License v2 (see forum.txt)

date

$Date: 2005/07/13 17:05:06 $

revision

$Revision: 1.19 $

class

KL_STDOUT_FILE

inherit

KI_TEXT_OUTPUT_STREAM
CONSOLE

create

make

-- Create a new standard output file.

ensure
name_set: name.is_equal (

stdout

)
is_open_write: is_open_write

feature -- Access

eol: STRING

-- Line separator

-- (From KI_TEXT_OUTPUT_STREAM)

ensure
eol_not_void: Result /= Void
eol_not_empty: Result.count > 0
file_pointer: POINTER

-- File pointer as required in C

-- (From FILE)

name: STRING

-- File name

-- (From KI_OUTPUT_STREAM)

ensure
name_not_void: Result /= Void

feature -- Status report

count: INTEGER

-- Useless for CONSOLE class.
--| count is non null not to invalidate invariant clauses.

-- (From FINITE)

extendible: BOOLEAN

-- May new items be added?

-- (From COLLECTION)

is_closable: BOOLEAN

-- Can current output stream be closed?

-- (From KI_OUTPUT_STREAM)

ensure
is_open: Result implies is_open_write
is_closed: BOOLEAN

-- Is file closed?

-- (From IO_MEDIUM)

is_open_write: BOOLEAN

-- Is standard output file opened in write mode?

-- (From KI_OUTPUT_STREAM)

old_is_open_write: BOOLEAN

-- Is file open for writing?

-- (From IO_MEDIUM)

feature -- Status setting

old_close

-- Close file.

-- (From IO_MEDIUM)

require
medium_is_open: not is_closed
ensure then
is_closed: is_closed
open_read

-- Open file in read-only mode.

-- (From FILE)

require
is_closed: is_closed
ensure
exists: exists
open_read: is_open_read

feature -- Basic operations

close

-- Try to close output stream if it is closable. Set
-- is_open_write to false if operation was successful.

-- (From KI_OUTPUT_STREAM)

require
is_closable: is_closable
flush

-- Flush buffered data to disk.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write

feature -- Output

append (an_input_stream: KI_INPUT_STREAM [CHARACTER])

-- Read items of an_input_stream until the end
-- of input is reached, and write these items to
-- current output stream.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
an_input_stream_not_void: an_input_stream /= Void
an_input_stream_open_read: an_input_stream.is_open_read
ensure
end_of_input: an_input_stream.end_of_input
old_put_string (s: STRING)

-- Write s at end of default output.

-- (From IO_MEDIUM)

require
extendible: extendible
non_void: s /= Void
put_boolean (b: BOOLEAN)

-- Write "True" to output stream if
-- b is true, "False" otherwise.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_character (c: CHARACTER)

-- Write c to standard output file.

-- (From KI_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_integer (i: INTEGER)

-- Write decimal representation
-- of i to output stream.
-- Regexp: 0|(-?[1-9][0-9]*)

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_line (a_string: STRING)

-- Write a_string to output stream
-- followed by a line separator.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
put_new_line

-- Write a line separator to output stream.

-- (From KI_TEXT_OUTPUT_STREAM)

require
is_open_write: is_open_write
put_string (a_string: STRING)

-- Write a_string to standard output file.
-- Note: If a_string is a UC_STRING or descendant, then
-- write the bytes of its associated UTF unicode encoding.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
put_substring (a_string: STRING; s, e: INTEGER)

-- Write substring of a_string between indexes
-- s and e to output stream.

-- (From KI_CHARACTER_OUTPUT_STREAM)

require
is_open_write: is_open_write
a_string_not_void: a_string /= Void
s_large_enough: s >= 1
e_small_enough: e <= a_string.count
valid_interval: s <= e + 1

invariant


-- From ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)

-- From PLAIN_TEXT_FILE
plain_text: is_plain_text

-- From FILE
valid_mode: Closed_file <= mode and mode <= Append_read_file
name_exists: name /= Void
name_not_empty: not name.is_empty

-- From FINITE
empty_definition: is_empty = (count = 0)
non_negative_count: count >= 0

-- From ACTIVE
writable_constraint: writable implies readable
empty_constraint: is_empty implies (not readable) and (not writable)

-- From BILINEAR
not_both: not (after and before)
before_constraint: before implies off

-- From LINEAR
after_constraint: after implies off

-- From TRAVERSABLE
empty_constraint: is_empty implies off

end