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

kernel.spec.ise

Class KL_STDIN_FILE


Direct ancestors

KI_TEXT_INPUT_STREAM, KL_OPERATING_SYSTEM, KL_IMPORTED_ANY_ROUTINES, CONSOLE

Creation

Features

Invariants

indexing

description

Standard input files containing extended ASCII characters %
%(8-bit code between 0 and 255). The line separtor of the %
%underlying file system is automatically converted to %%N %
%when read from the satndard input file. However read_line %
%and read_new_line are able to recognize '%%N', '%%R%%N' %
%and '%%R' as line separators.

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.23 $

class

KL_STDIN_FILE

inherit

KI_TEXT_INPUT_STREAM
CONSOLE

create

make

-- Create a new standard input file.

ensure
name_set: name.is_equal (

stdin

)
is_open_read: is_open_read
not_end_of_file: not end_of_file

feature -- Access

any_: KL_ANY_ROUTINES

-- Routines that ought to be in class ANY

-- (From KL_IMPORTED_ANY_ROUTINES)

ensure
any_routines_not_void: Result /= Void
eol: STRING

-- Line separator

-- (From KI_TEXT_INPUT_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_INPUT_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)

end_of_file: BOOLEAN

-- Has the end of file been reached?

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
extendible: BOOLEAN

-- May new items be added?

-- (From COLLECTION)

is_closable: BOOLEAN

-- Can current input stream be closed?

-- (From KI_INPUT_STREAM)

ensure
is_open: Result implies is_open_read
is_closed: BOOLEAN

-- Is file closed?

-- (From IO_MEDIUM)

is_open_read: BOOLEAN

-- Is standard input file opened in read mode?

-- (From KI_INPUT_STREAM)

is_open_write: BOOLEAN

-- Is file open for writing?

-- (From IO_MEDIUM)

is_rewindable: BOOLEAN

-- Can current input stream be rewound to return input from
-- the beginning of the stream?

-- (From KI_INPUT_STREAM)

ensure
rewind_implies_open: Result implies is_open_read
last_character: CHARACTER

-- Last character read by read_character

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
last_string: STRING

-- Last string read

-- (From KI_CHARACTER_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
ensure
string_type: Result /= Void implies ANY_.same_types (Result,
)
valid_unread_character (a_character: CHARACTER): BOOLEAN

-- Can a_character be put back in input stream?

-- (From KI_INPUT_STREAM)

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 input stream if it is closable. Set
-- is_open_read to false if operation was successful.

-- (From KI_INPUT_STREAM)

require
is_closable: is_closable
rewind

-- Move input position to the beginning of stream.

-- (From KI_INPUT_STREAM)

require
can_rewind: is_rewindable

feature -- Input

read_character

-- Read the next character in standard input file.
-- Make the result available in last_character.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
read_line

-- Read characters from standard input file until a line separator
-- or end of file is reached. Make the characters that have
-- been read available in last_string and discard the line
-- separator characters from the standard input file.
-- Line separators recognized by current standard input
-- file are: '%N', '%R%N and '%R'.

-- (From KI_TEXT_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
ensure
last_string_not_void: not end_of_input implies last_string /= Void
read_new_line

-- Read a line separator from standard input file.
-- Make the characters making up the recognized
-- line separator available in last_string,
-- or make last_string empty and leave the
-- standard input file unchanged if no line
-- separator was found.
-- Line separators recognized by current standard
-- input file are: '%N', '%R%N and '%R'.

-- (From KI_TEXT_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
ensure
not_end_of_input: not end_of_input
last_string_not_void: last_string /= Void
read_string (nb: INTEGER)

-- Read at most nb characters from standard input file.
-- Make the characters that have actually been read
-- available in last_string.

-- (From KI_CHARACTER_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
nb_large_enough: nb > 0
ensure
last_string_not_void: not end_of_input implies last_string /= Void
last_string_count_small_enough: not end_of_input implies last_string.count <= nb
character_read: not end_of_input implies last_string.count > 0
read_to_buffer (a_buffer: KI_BUFFER [CHARACTER]; pos, nb: INTEGER): INTEGER

-- Fill a_buffer, starting at position pos, with
-- at most nb characters read from standard input file.
-- Return the number of characters actually read.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
a_buffer_not_void: a_buffer /= Void
pos_large_enough: pos >= 1
nb_large_enough: nb > 0
enough_space: (pos + nb - 1) <= a_buffer.count
ensure
nb_item_read_large_enough: Result >= 0
nb_item_read_small_enough: Result <= nb
not_end_of_input: not end_of_input implies Result > 0
read_to_string (a_string: STRING; pos, nb: INTEGER): INTEGER

-- Fill a_string, starting at position pos with at
-- most nb characters read from standard input file.
-- Return the number of characters actually read.

-- (From KI_CHARACTER_INPUT_STREAM)

require
is_open_read: is_open_read
not_end_of_input: not end_of_input
a_string_not_void: a_string /= Void
valid_position: a_string.valid_index (pos)
nb_large_enough: nb > 0
nb_small_enough: nb <= a_string.count - pos + 1
ensure
nb_char_read_large_enough: Result >= 0
nb_char_read_small_enough: Result <= nb
character_read: not end_of_input implies Result > 0
unread_character (a_character: CHARACTER)

-- Put a_character back in input file.
-- This character will be read first by the next
-- call to a read routine.

-- (From KI_INPUT_STREAM)

require
is_open_read: is_open_read
an_item_valid: valid_unread_item (an_item)
ensure
not_end_of_input: not end_of_input
last_item_set: last_item = an_item

feature -- Output

put_string (s: STRING)

-- Write s at end of default output.

-- (From IO_MEDIUM)

require
extendible: extendible
non_void: s /= Void

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