equal
deleted
inserted
replaced
77 Position.Line_File(source_content.position(range.start).line1, file.implode) ::: |
77 Position.Line_File(source_content.position(range.start).line1, file.implode) ::: |
78 Position.Range(symbol_range) |
78 Position.Range(symbol_range) |
79 } |
79 } |
80 |
80 |
81 def tex_position(line: Int): Position.T = |
81 def tex_position(line: Int): Position.T = |
82 Position.File(tex_file.implode) ::: Position.Line(line) |
82 Position.Line_File(line, tex_file.implode) |
83 |
83 |
84 def position(line: Int): Position.T = |
84 def position(line: Int): Position.T = |
85 source_position(line) getOrElse tex_position(line) |
85 source_position(line) getOrElse tex_position(line) |
86 } |
86 } |
87 |
87 |
139 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) |
139 @tailrec def filter(lines: List[String], result: List[(String, Position.T)]) |
140 : List[(String, Position.T)] = |
140 : List[(String, Position.T)] = |
141 { |
141 { |
142 lines match { |
142 lines match { |
143 case File_Line_Error((file, line, msg1)) :: rest1 => |
143 case File_Line_Error((file, line, msg1)) :: rest1 => |
144 val pos = tex_file_position(file, line) |
144 val pos = tex_file_position((dir + file).canonical, line) |
145 rest1 match { |
145 rest1 match { |
146 case Line_Error((line2, msg2)) :: rest2 if line == line2 => |
146 case Line_Error((line2, msg2)) :: rest2 if line == line2 => |
147 filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) |
147 filter(rest2, (Exn.cat_message(msg1, msg2), pos) :: result) |
148 case _ => |
148 case _ => |
149 filter(rest1, (msg1, pos) :: result) |
149 filter(rest1, (msg1, pos) :: result) |