equal
deleted
inserted
replaced
33 progress: Progress, |
33 progress: Progress, |
34 keywords: Keyword.Keywords, |
34 keywords: Keyword.Keywords, |
35 check: Set[String], |
35 check: Set[String], |
36 paths: List[Path] |
36 paths: List[Path] |
37 ): Unit = { |
37 ): Unit = { |
38 val parallel_args = paths.map(path => (File.read(path), Token.Pos.file(path.expand.implode))) |
38 val parallel_args = |
|
39 paths.map(path => (File.read(path), Token.Pos.file(File.standard_path(path)))) |
39 |
40 |
40 val bad = |
41 val bad = |
41 Par_List.map({ (arg: (String, Token.Pos)) => |
42 Par_List.map({ (arg: (String, Token.Pos)) => |
42 progress.expose_interrupt() |
43 progress.expose_interrupt() |
43 conflicts(keywords, check, arg._1, arg._2) |
44 conflicts(keywords, check, arg._1, arg._2) |