Eiffeldoc: REGULAR_EXPRESSION_STRING_SCANNER

+

Point of view

All features

class REGULAR_EXPRESSION_STRING_SCANNER

Summary

Facility to scan strings TODO improve it by using STRING_HANDLER and string's storage

Direct parents: Insert list: ANY
Known children: Insert list: BACKTRACKING_REGULAR_EXPRESSION, BACKTRACKING_REGULAR_EXPRESSION_BUILDER

Class invariant

last_string_not_void: last_string /= Void

Overview

Features

make

make

Initialise the attributes.

basic

scanned_string: ABSTRACT_STRING

The expression being currently build.
set_scanned_string (string: ABSTRACT_STRING)

Set the 'scanned_string' with 'string'.

error management

has_error: BOOLEAN

True when an error was encountered
clear_error

Remove the error flag
last_error: STRING

Returns a string recorded for the error.
set_error (message: STRING)

Set has_error and last_error.

scanning

position: INTEGER_32

The scanned position.
last_character: CHARACTER

The scanned character.
valid_last_character: BOOLEAN

True when 'last_character' is valid.
valid_previous_character: BOOLEAN

True if the position-1 is a valid position.
previous_character: CHARACTER

The character at position-1.
valid_next_character: BOOLEAN

True if the position+1 is a valid position.
next_character: CHARACTER

The character at position+1.
end_of_input: BOOLEAN

True when all the characters of 'scanned_string' are scanned.
goto_position (pos: INTEGER_32)

Change the currently scanned position to 'pos'.
read_character

Reads the next character.
read_integer

Reads an integer value beginning at the currently scanned position.
saved_position: INTEGER_32

The saved position (only one is currently enough).
save_position

Saves the current scanning position.
restore_saved_position

Restore the scanning position to the last saved one.
last_string: STRING

A string buffer.
last_integer: INTEGER_32

An integer buffer.

make

effective procedure

Initialise the attributes.

scanned_string: ABSTRACT_STRING

writable attribute

The expression being currently build.

set_scanned_string (string: ABSTRACT_STRING)

effective procedure

Set the 'scanned_string' with 'string'.

ensure

has_no_error: not has_error
definition: scanned_string = string
at_the_begin: position = scanned_string.lower

has_error: BOOLEAN

writable attribute

True when an error was encountered

clear_error

effective procedure

Remove the error flag

ensure

has_no_error: not has_error

last_error: STRING

effective function

Returns a string recorded for the error.

require

has_error: has_error

ensure

not_void: Result /= Void

set_error (message: STRING)

effective procedure

Set has_error and last_error.

The explaining error string 'last_error' is created as follow: "Error at position 'position': 'message'.".

require

message_not_void: message /= Void
has_no_error: not has_error

ensure

has_error: has_error

position: INTEGER_32

writable attribute

The scanned position.

It is the position of 'last_character'.

last_character: CHARACTER

writable attribute

The scanned character.

The last character read from 'scanned_string'.

valid_last_character: BOOLEAN

writable attribute

True when 'last_character' is valid.

Is like 'scanned_string.valid_index(position)'

valid_previous_character: BOOLEAN

effective function

True if the position-1 is a valid position.

require

scanned_string /= Void

ensure

definition: Result = scanned_string.valid_index(position - 1)

previous_character: CHARACTER

effective function

The character at position-1.

require

valid_previous_character

ensure

definition: Result = scanned_string.item(position - 1)

valid_next_character: BOOLEAN

effective function

True if the position+1 is a valid position.

require

scanned_string /= Void

ensure

definition: Result = scanned_string.valid_index(position + 1)

next_character: CHARACTER

effective function

The character at position+1.

require

valid_next_character

ensure

definition: Result = scanned_string.item(position + 1)

end_of_input: BOOLEAN

effective function

True when all the characters of 'scanned_string' are scanned.

ensure

implies_last_character_not_valid: Result implies not valid_last_character

goto_position (pos: INTEGER_32)

effective procedure

Change the currently scanned position to 'pos'.

Updates 'last_character' and 'valid_last_character' to reflect the new position value.

require

has_no_error: not has_error
scanned_string /= Void

ensure

has_no_error: not has_error
position_set: position = pos
validity_updated: valid_last_character = scanned_string.valid_index(position)
character_updated: valid_last_character implies last_character = scanned_string.item(position)

read_character

effective procedure

Reads the next character.

require

has_no_error: not has_error
not_at_end: not end_of_input

ensure

next_position: position > old position
has_no_error: not has_error

read_integer

effective procedure

Reads an integer value beginning at the currently scanned position.

The read value is stored in 'last_integer'.

require

has_no_error: not has_error
not_at_end: not end_of_input
begin_with_a_digit: last_character.is_decimal_digit

ensure

has_no_error: not has_error
digits_eaten: end_of_input or else not last_character.is_decimal_digit

saved_position: INTEGER_32

writable attribute

The saved position (only one is currently enough).

save_position

effective procedure

Saves the current scanning position.

require

not_at_end: not end_of_input

ensure

not_at_end: not end_of_input
position_kept: position = old position
saved_position_set: saved_position = position

restore_saved_position

effective procedure

Restore the scanning position to the last saved one.

ensure

position_restored: position = old saved_position
not_at_end: not end_of_input

last_string: STRING

writable attribute

A string buffer.

last_integer: INTEGER_32

writable attribute

An integer buffer.