class interface HELP_ON_HELP 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? invariant valid_parent: parent /= Void; valid_help: helpfile /= Void; end of HELP_ON_HELP