+%{
+ int lineno IF_LINT (= 0);
+ char *outname = NULL;
+%}
+
+"@output ".*\n {
+ char const *filename = yytext + sizeof "@output " - 1;
+ yytext[yyleng - 1] = '\0';
+
+ if (*filename == '@')
+ {
+ if (strcmp (filename, "@output_header_name@") == 0)
+ filename = spec_defines_file;
+ else if (strcmp (filename, "@output_parser_name@") == 0)
+ filename = parser_file_name;
+ else
+ abort ();
+ }
+
+ XFREE (outname);
+ outname = xstrdup (filename);
+ xfclose (yyout);
+ yyout = xfopen (outname, "w");
+ lineno = 1;
+}
+
+"@@" fputc ('@', yyout);
+"@{" fputc ('[', yyout);
+"@}" fputc (']', yyout);
+
+"@oline@" fprintf (yyout, "%d", lineno + 1);
+"@ofile@" QPUTS (outname);
+"@output_parser_name@" QPUTS (parser_file_name);
+"@output_header_name@" QPUTS (spec_defines_file);
+
+"@" abort ();
+\n lineno++; ECHO;
+[^@\n]+ ECHO;
+
+<<EOF>> xfclose (yyout); free (outname); return EOF;