equal
deleted
inserted
replaced
35 } |
35 } |
36 |
36 |
37 if (content.contains('\r')) |
37 if (content.contains('\r')) |
38 Output.warning("CR character" + Position.here(file_pos)) |
38 Output.warning("CR character" + Position.here(file_pos)) |
39 } |
39 } |
|
40 |
|
41 def check_hg(root: Path) |
|
42 { |
|
43 System.err.println("Checking " + root + " ...") |
|
44 Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error |
|
45 for { |
|
46 file <- Isabelle_System.hg("manifest", root).check_error.out_lines |
|
47 if file.endsWith(".thy") || file.endsWith(".ML") |
|
48 } check_file(root + Path.explode(file)) |
|
49 } |
|
50 |
|
51 |
|
52 /* command line entry point */ |
|
53 |
|
54 def main(args: Array[String]) |
|
55 { |
|
56 Command_Line.tool0 { |
|
57 for (root <- args) check_hg(Path.explode(root)) |
|
58 } |
|
59 } |
40 } |
60 } |
41 |
61 |