1%{
2#define YY_USER_INIT open_input_file()
3
4extern FILE *yyin;
5
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