class interface HELP_KEYWORD creation make (par: WINDOW) -- Create this object. require valid_window: par /= Void ensure keep_reference: par = parent feature(s) from GUI_COMMAND execute -- Execute help command ensure done: -- last_command_success set. feature(s) from HELP_COMMAND -- Status set_helpfile (str: STRING) -- Set the current helpfile. require valid_str: str /= Void; -- str must be path to valid helpfile. valid_help: feature(s) from HELP_COMMAND -- Command last_command_success: BOOLEAN -- Was the last request succesful? feature(s) from HELP_KEYWORD -- Attribute(s) key: STRING set_key (str: STRING) require valid_string: str /= Void ensure keep_reference: key = str invariant valid_parent: parent /= Void; valid_help: helpfile /= Void; end of HELP_KEYWORD