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