deferred class interface HELP_COMMAND

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 deferred HELP_COMMAND