class interface HELP_CONTENTS

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_CONTENTS