1 /* Title: Pure/Tools/check_source.scala |
|
2 Author: Makarius |
|
3 |
|
4 Some sanity checks for Isabelle sources. |
|
5 */ |
|
6 |
|
7 package isabelle |
|
8 |
|
9 |
|
10 object Check_Source |
|
11 { |
|
12 def check_file(path: Path) |
|
13 { |
|
14 val file_name = path.implode |
|
15 val file_pos = path.position |
|
16 def line_pos(i: Int) = Position.Line_File(i + 1, file_name) |
|
17 |
|
18 val content = File.read(path) |
|
19 |
|
20 for { (line, i) <- split_lines(content).iterator.zipWithIndex } |
|
21 { |
|
22 try { |
|
23 Symbol.decode_strict(line) |
|
24 |
|
25 for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) } |
|
26 { |
|
27 Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) + |
|
28 Position.here(line_pos(i))) |
|
29 } |
|
30 } |
|
31 catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) } |
|
32 |
|
33 if (line.contains('\t')) |
|
34 Output.warning("TAB character" + Position.here(line_pos(i))) |
|
35 } |
|
36 |
|
37 if (content.contains('\r')) |
|
38 Output.warning("CR character" + Position.here(file_pos)) |
|
39 } |
|
40 |
|
41 def check_hg(root: Path) |
|
42 { |
|
43 Output.writeln("Checking " + root + " ...") |
|
44 Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check |
|
45 for { |
|
46 file <- Isabelle_System.hg("manifest", root).check.out_lines |
|
47 if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
|
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 } |
|
60 } |
|
61 |
|