Changed the WGI_INPUT_STREAM and WGI_OUTPUT_STREAM interfaces

main changes for existing code  `read_stream' is renamed `read_string'
This commit is contained in:
Jocelyn Fiat
2011-11-14 14:17:41 +01:00
parent bc2e8b8ee2
commit 13b09adc8c
19 changed files with 334 additions and 113 deletions

View File

@@ -336,7 +336,7 @@ feature {NONE} -- I/O: implementation
read_input (nb: INTEGER)
-- Read `nb' bytes from `input'
do
input.read_stream (nb)
input.read_string (nb)
end
last_input_string: STRING

View File

@@ -11,21 +11,108 @@ note
deferred class
WGI_INPUT_STREAM
feature -- Input
read_character
-- Read the next character in input stream.
-- Make the result available in `last_character'.
require
is_open_read: is_open_read
not_end_of_input: not end_of_input
deferred
ensure
same_last_string_reference: last_string = old last_string
end
read_string (nb: INTEGER)
require
is_open_read: is_open_read
not_end_of_input: not end_of_input
nb_large_enough: nb > 0
deferred
ensure
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
same_last_string_reference: last_string = old last_string
end
read_to_string (a_string: STRING; pos, nb: INTEGER): INTEGER
-- Fill `a_string', starting at position `pos', with
-- at most `nb' characters read from input stream.
-- Return the number of characters actually read.
-- (Note that even if at least `nb' characters are available
-- in the input stream, there is no guarantee that they
-- will all be read.)
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
local
i, end_pos: INTEGER
do
end_pos := pos + nb - 1
from
i := pos
until
i > end_pos
loop
read_character
if not end_of_input then
a_string.put (last_character, i)
i := i + 1
else
Result := i - pos - nb
-- Jump out of the loop.
i := end_pos + 1
end
end
Result := Result + i - pos
ensure
nb_char_read_large_enough: Result >= 0
nb_char_read_small_enough: Result <= nb
character_read: not end_of_input implies Result > 0
same_last_string_reference: last_string = old last_string
end
feature -- Access
last_string: STRING_8
-- Last read string from stream
-- Last string read
-- (Note: this query always return the same object.
-- Therefore a clone should be used if the result
-- is to be kept beyond the next call to this feature.
-- However `last_string' is not shared between file objects.)
require
is_open_read: is_open_read
not_end_of_input: not end_of_input
deferred
ensure
last_string_not_void: Result /= Void
end
last_character: CHARACTER_8
-- Last item read
require
is_open_read: is_open_read
not_end_of_input: not end_of_input
deferred
end
feature -- Basic operation
feature -- Status report
read_stream (n: INTEGER)
require
n_positive: n > 0
is_open_read: BOOLEAN
-- Can items be read from input stream?
deferred
end
end_of_input: BOOLEAN
-- Has the end of input stream been reached?
require
is_open_read: is_open_read
deferred
ensure
at_max_n: last_string.count <= n
end
note

View File

@@ -11,18 +11,70 @@ note
deferred class
WGI_OUTPUT_STREAM
feature -- Core operation
feature -- Output
put_string (s: STRING_8)
-- Write `s' into the output stream
put_string (a_string: STRING_8)
-- Write `a_string' to output stream.
require
s_not_empty: s /= Void and then not s.is_empty
is_open_write: is_open_write
a_string_not_void: a_string /= Void
deferred
end
flush
-- Flush the output stream
put_substring (a_string: STRING; s, e: INTEGER)
-- Write substring of `a_string' between indexes
-- `s' and `e' to output stream.
--| Could be redefined for optimization
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
do
if s <= e then
put_string (a_string.substring (s, e))
end
end
put_character_8 (c: CHARACTER_8)
-- Write `c' to output stream.
--| Could be redefined for optimization
require
is_open_write: is_open_write
do
put_string (c.out)
end
put_file_content (fn: STRING)
-- Send the content of file `fn'
require
string_not_empty: not fn.is_empty
is_readable: (create {RAW_FILE}.make (fn)).is_readable
local
f: RAW_FILE
do
create f.make (fn)
check f.exists and then f.is_readable end
f.open_read
from
until
f.exhausted
loop
f.read_stream (4096)
put_string (f.last_string)
end
f.close
end
feature -- Specific output
put_header_line (s: STRING)
-- Send `s' to http client as header line
do
put_string (s)
put_string ("%R%N")
end
feature -- Status writing
@@ -34,41 +86,20 @@ feature -- Status writing
deferred
end
feature -- Basic operation
feature -- Status report
put_substring (s: STRING; start_index, end_index: INTEGER)
-- Write `s[start_index:end_index]' into the output stream
--| Could be redefined for optimization
is_open_write: BOOLEAN
-- Can items be written to output stream?
deferred
end
feature -- Basic operations
flush
-- Flush buffered data to disk.
require
s_not_empty: s /= Void and then not s.is_empty
do
put_string (s.substring (start_index, end_index))
end
put_file_content (fn: STRING)
-- Send the content of file `fn'
local
f: RAW_FILE
do
create f.make (fn)
if f.exists and then f.is_readable then
f.open_read
from
until
f.exhausted
loop
f.read_stream (4096)
put_string (f.last_string)
end
f.close
end
end
put_header_line (s: STRING)
-- Send `s' to http client as header line
do
put_string (s)
put_string ("%R%N")
is_open_write: is_open_write
deferred
end
note