equal
deleted
inserted
replaced
107 line match { |
107 line match { |
108 case Pattern(file, Value.Int(line), message) => |
108 case Pattern(file, Value.Int(line), message) => |
109 val path = File.standard_path(file) |
109 val path = File.standard_path(file) |
110 if (Path.is_wellformed(path)) { |
110 if (Path.is_wellformed(path)) { |
111 val file = (dir + Path.explode(path)).canonical |
111 val file = (dir + Path.explode(path)).canonical |
112 if (file.is_file) Some((file, line, message)) else None |
112 val msg = Library.perhaps_unprefix("LaTeX Error: ", message) |
|
113 if (file.is_file) Some((file, line, msg)) else None |
113 } |
114 } |
114 else None |
115 else None |
115 case _ => None |
116 case _ => None |
116 } |
117 } |
117 } |
118 } |
134 "<everycr>", |
135 "<everycr>", |
135 "<mark>", |
136 "<mark>", |
136 "<everyeof>", |
137 "<everyeof>", |
137 "<write>").mkString("^(?:", "|", ") (.*)$").r |
138 "<write>").mkString("^(?:", "|", ") (.*)$").r |
138 |
139 |
|
140 val error_ignore = |
|
141 Set( |
|
142 "See the LaTeX manual or LaTeX Companion for explanation.", |
|
143 "Type H <return> for immediate help.") |
|
144 |
139 def error_suffix1(lines: List[String]): Option[String] = |
145 def error_suffix1(lines: List[String]): Option[String] = |
140 { |
146 { |
141 val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true }) |
147 val lines1 = lines.take(20).takeWhile({ case File_Line_Error(_) => false case _ => true }) |
142 lines1.zipWithIndex.collectFirst({ |
148 lines1.zipWithIndex.collectFirst({ |
143 case (Line_Error(msg), i) => cat_lines(lines1.take(i) ::: List(msg)) }) |
149 case (Line_Error(msg), i) => |
|
150 cat_lines(lines1.take(i).filterNot(error_ignore) ::: List(msg)) }) |
144 } |
151 } |
145 def error_suffix2(lines: List[String]): Option[String] = |
152 def error_suffix2(lines: List[String]): Option[String] = |
146 lines match { |
153 lines match { |
147 case More_Error(msg) :: _ => Some(msg) |
154 case More_Error(msg) :: _ => Some(msg) |
148 case _ => None |
155 case _ => None |