extern void read_command_file PARAMS ((FILE *));
extern void init_history PARAMS ((void));
extern void command_loop PARAMS ((void));
extern void read_command_file PARAMS ((FILE *));
extern void init_history PARAMS ((void));
extern void command_loop PARAMS ((void));