const char *current_filename = 0;
const char *current_source_filename = 0;