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