136 "<everycr>", |
136 "<everycr>", |
137 "<mark>", |
137 "<mark>", |
138 "<everyeof>", |
138 "<everyeof>", |
139 "<write>").mkString("^(?:", "|", ") (.*)$").r |
139 "<write>").mkString("^(?:", "|", ") (.*)$").r |
140 |
140 |
|
141 val Bad_Font = """^LaTeX Font Warning: (Font .*\btxmia\b.* undefined).*$""".r |
141 val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r |
142 val Bad_File = """^! LaTeX Error: (File `.*' not found\.)$""".r |
142 |
143 |
143 val error_ignore = |
144 val error_ignore = |
144 Set( |
145 Set( |
145 "See the LaTeX manual or LaTeX Companion for explanation.", |
146 "See the LaTeX manual or LaTeX Companion for explanation.", |
165 lines match { |
166 lines match { |
166 case File_Line_Error((file, line, msg1)) :: rest1 => |
167 case File_Line_Error((file, line, msg1)) :: rest1 => |
167 val pos = tex_file_position(file, line) |
168 val pos = tex_file_position(file, line) |
168 val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse "" |
169 val msg2 = error_suffix1(rest1) orElse error_suffix2(rest1) getOrElse "" |
169 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result) |
170 filter(rest1, (Exn.cat_message(msg1, msg2), pos) :: result) |
|
171 case Bad_Font(msg) :: rest => |
|
172 filter(rest, (msg, Position.none) :: result) |
170 case Bad_File(msg) :: rest => |
173 case Bad_File(msg) :: rest => |
171 filter(rest, (msg, Position.none) :: result) |
174 filter(rest, (msg, Position.none) :: result) |
172 case _ :: rest => filter(rest, result) |
175 case _ :: rest => filter(rest, result) |
173 case Nil => result.reverse |
176 case Nil => result.reverse |
174 } |
177 } |