class interface REGISTRY_KEY
creation
make_user
-- Create registry object based on current USER.
make_machine
-- Create registry object based on current MACHINE.
feature(s) from MEMORY
-- Removal :
dispose
full_collect
-- Force a full collection cycle if garbage collection is
-- enabled; do nothing otherwise.
feature(s) from REGISTRY_KEY
-- Actions
is_open: BOOLEAN
-- Is the current key open?
is_new: BOOLEAN
-- Has the current key just been created?
require
open: is_open
open (name: STRING)
-- Open an existing registry key.
require
valid_name: name /= Void;
closed: not is_open
ensure
not_new: is_new = false; -- check is_open.
may_fail:
create_key (name: STRING)
-- Create a new key (or open an existing one).
require
valid_name: name /= Void;
closed: not is_open
ensure
may_fail: -- check is_open.
close
-- Close the current key.
require
opened: is_open
ensure
closed: not is_open
feature(s) from REGISTRY_KEY
-- Utility
standard_name (company, program, key: STRING): STRING
-- Return a standard key name for Software configuration.
-- (that is "Software\\\")
require
valid_company: company /= Void;
valid_program: program /= Void;
valid_key: key /= Void
feature(s) from REGISTRY_KEY
-- List of values/subkeys
values: DS_LIST[STRING]
-- Enumerate value labels of this key.
require
open: is_open
ensure
is_copy: Result /= Void
subkeys: DS_LIST[STRING]
-- Enumerate subkey names associated under this key.
require
open: is_open
ensure
is_copy: Result /= Void
delete_subkey (name: STRING)
-- Delete subkey.
-- Note: delete does not recurse under Windows NT.
require
ok: name /= Void; -- has_subkey (name)
exists:
feature(s) from REGISTRY_KEY
-- Last read value.
has_value: BOOLEAN
-- Was last read operation successful?
last_string: STRING
-- Last read string.
require
ready: has_value
ensure
done: Result /= Void; -- New string for each read (not for each call to last_string).
copy:
last_integer: INTEGER
-- Last read integer.
require
ready: has_value
last_boolean: BOOLEAN
-- Last read boolean.
require
ready: has_value
feature(s) from REGISTRY_KEY
-- Read
read_string (label: STRING)
-- Read a string key value.
require
valid: label /= Void;
open: is_open
ensure
may_fail: -- has_value implies last_string set
read_integer (label: STRING)
-- Read an integer key value.
require
valid: label /= Void;
open: is_open
ensure
may_fail: -- has_value implies last_integer set
read_boolean (label: STRING)
-- Read a pseudo-boolean key value (actually an integer).
require
valid: label /= Void;
open: is_open
ensure
may_fail: -- has_value implies last_boolean set
feature(s) from REGISTRY_KEY
-- Write
write_boolean (label: STRING; value: BOOLEAN)
-- Write a pseudo-boolean (actually an integer value
-- to the registry.
require
open: is_open;
valid_label: label /= Void
write_integer (label: STRING; value: INTEGER)
-- Write an integer in the registry.
require
open: is_open;
valid_label: label /= Void
write_string (label: STRING; value: STRING)
-- Write a string to the registry.
require
open: is_open;
valid_label: label /= Void;
valid_value: value /= Void
end of REGISTRY_KEY