const char *current_filename = 0;