equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 import java.io.{File => JFile} |
10 import java.io.{File => JFile} |
11 |
11 |
12 import scala.annotation.tailrec |
12 import scala.annotation.tailrec |
|
13 import scala.util.matching.Regex |
13 |
14 |
14 |
15 |
15 object Latex |
16 object Latex |
16 { |
17 { |
17 /** latex errors **/ |
18 /** latex errors **/ |
100 case None => Position.Line_File(line, path.implode) |
101 case None => Position.Line_File(line, path.implode) |
101 } |
102 } |
102 |
103 |
103 object File_Line_Error |
104 object File_Line_Error |
104 { |
105 { |
105 val Pattern = """^(.*?\.\w\w\w):(\d+): (.*)$""".r |
106 val Pattern: Regex = """^(.*?\.\w\w\w):(\d+): (.*)$""".r |
106 def unapply(line: String): Option[(Path, Int, String)] = |
107 def unapply(line: String): Option[(Path, Int, String)] = |
107 line match { |
108 line match { |
108 case Pattern(file, Value.Int(line), message) => |
109 case Pattern(file, Value.Int(line), message) => |
109 val path = File.standard_path(file) |
110 val path = File.standard_path(file) |
110 if (Path.is_wellformed(path)) { |
111 if (Path.is_wellformed(path)) { |