static void refreshoptions(void);static void readstream(FILE* stream);