114 else None |
114 else None |
115 case _ => None |
115 case _ => None |
116 } |
116 } |
117 } |
117 } |
118 |
118 |
119 object Line_Error |
119 val More_Error = |
120 { |
120 List( |
121 val Pattern = """^l\.(\d+) (.*)$""".r |
121 """l\.\d+""", |
122 def unapply(line: String): Option[(Int, String)] = |
122 "<argument>", |
123 line match { |
123 "<template>", |
124 case Pattern(Value.Int(line), message) => Some((line, message)) |
124 "<recently read>", |
125 case _ => None |
125 "<to be read again>", |
126 } |
126 "<inserted text>", |
127 } |
127 "<output>", |
|
128 "<everypar>", |
|
129 "<everymath>", |
|
130 "<everydisplay>", |
|
131 "<everyhbox>", |
|
132 "<everyvbox>", |
|
133 "<everyjob>", |
|
134 "<everycr>", |
|
135 "<mark>", |
|
136 "<everyeof>", |
|
137 "<write>").mkString("^(?:", "|", ") (.*)$").r |
128 |
138 |
129 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) |
139 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) |
130 : List[(String, Position.T)] = |
140 : List[(String, Position.T)] = |
131 { |
141 { |
132 lines match { |
142 lines match { |
133 case File_Line_Error((file, line, msg1)) :: rest1 => |
143 case File_Line_Error((file, line, msg1)) :: rest1 => |
134 val pos = tex_file_position(file, line) |
144 val pos = tex_file_position(file, line) |
135 rest1 match { |
145 rest1 match { |
136 case Line_Error((line2, msg2)) :: rest2 if line == line2 => |
146 case More_Error(msg2) :: rest2 => |
137 filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) |
147 filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) |
138 case _ => |
148 case _ => |
139 filter(rest1, (msg1, pos) :: result) |
149 filter(rest1, (msg1, pos) :: result) |
140 } |
150 } |
141 case _ :: rest => filter(rest, result) |
151 case _ :: rest => filter(rest, result) |