1 %{ 2 #define YY_USER_INIT open_input_file() 3 4 extern FILE *yyin; 5 open_input_file(void)6void open_input_file(void) 7 { 8 char *file_name,buffer[1024]; 9 10 yyin = NULL; 11 12 while(yyin == NULL){ 13 printf("Input file: "); 14 file_name = fgets(buffer,1024,stdin); 15 if(file_name){ 16 file_name[strlen(file_name)-1] = '\0'; 17 yyin = fopen(file_name,"r"); 18 if(yyin == NULL){ 19 printf("Unable to open \"%s\"\n",file_name); 20 } 21 } else { 22 printf("stdin\n"); 23 yyin = stdin; 24 break; 25 } 26 } 27 } 28 29 %} 30 %% 31