+ printf("File \"%s\"; Line %d", p, ErrorReport.line_number);
+
+ if (ErrorReport.orig_file) {
+ char *op;
+ if (ErrorReport.orig_file <= 0 || ErrorReport.orig_file > total_files)
+ op = ErrorReport.orig_source;
+ else
+ op = InputFiles[ErrorReport.orig_file-1].filename;
+ printf(": (\"%s\"", op);
+ if (ErrorReport.orig_line) {
+ printf("; Line %d", ErrorReport.orig_line);
+ if (ErrorReport.orig_char) {
+ printf("; Char %d", ErrorReport.orig_char);
+ }
+ }
+ printf(")");
+ }
+
+ printf("\t# ");