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