indexing
     description: ""
     date: "$Date$"
     revision: "$Revision$"

class interface
     LOGIN [G -> DATABASE create default_create end]

create

     make

feature -- Initialization

     make
     
feature -- Access

     db_spec: DATABASE
                 -- Handle to actual database
                 -- (from HANDLE_SPEC)
           ensure -- from HANDLE_SPEC
                 not_void: Result /= void
     
feature -- Status report

     application: STRING
                 -- Application name.

     data_source: STRING
                 -- Data Source.

     groupid: STRING
                 -- Group Identifier.

     hostname: STRING
                 -- Host name

     name: STRING
                 -- User name

     passwd: STRING
                 -- User password

     roleid: STRING
                 -- Role identifier .

     rolepasswd: STRING
                 -- Role password.
     
feature -- Status setting

     set (uname, upasswd: STRING)
                 -- Set user name and password before connection becomes possible.
           require
                 user_name_ok: db_spec.user_name_ok (uname)
                 password_ok: db_spec.password_ok (upasswd)
           ensure
                 password_ensure: db_spec.password_ensure (name, passwd, uname, upasswd)

     set_application (appname: STRING)
                 -- Set name of application
           require
                 argument_not_void: appname /= void
           ensure
                 name_set: application.is_equal (appname)

     set_data_source (udata_source: STRING)
                 -- Set Data Source of ODBC.
           require
                 argument_not_void: data_source /= void

     set_group (ugroupid: STRING)
           require
                 argument_not_void: ugroupid /= void
           ensure
                 name_set: groupid.is_equal (ugroupid)

     set_hostname (uhostname: STRING)
           require
                 argument_not_void: uhostname /= void
           ensure
                 name_set: hostname.is_equal (uhostname)

     set_role (uroleid, urolepasswd: STRING)
                 -- Set role identifier of data base.
           require
                 argument_not_void: uroleid /= void
           ensure
                 name_set: roleid.is_equal (uroleid)
     
invariant

           -- from ANY
     reflexive_equality: standard_is_equal (Current)
     reflexive_conformance: conforms_to (Current)

end -- class LOGIN