equal
deleted
inserted
replaced
5 */ |
5 */ |
6 |
6 |
7 package isabelle |
7 package isabelle |
8 |
8 |
9 |
9 |
10 object Check_Sources |
10 object Check_Sources { |
11 { |
11 def check_file(path: Path): Unit = { |
12 def check_file(path: Path): Unit = |
|
13 { |
|
14 val file_name = path.implode |
12 val file_name = path.implode |
15 val file_pos = path.position |
13 val file_pos = path.position |
16 def line_pos(i: Int) = Position.Line_File(i + 1, file_name) |
14 def line_pos(i: Int) = Position.Line_File(i + 1, file_name) |
17 |
15 |
18 if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux")) |
16 if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux")) |
23 |
21 |
24 if (Bytes(content) != bytes) { |
22 if (Bytes(content) != bytes) { |
25 Output.warning("Bad UTF8 encoding" + Position.here(file_pos)) |
23 Output.warning("Bad UTF8 encoding" + Position.here(file_pos)) |
26 } |
24 } |
27 |
25 |
28 for { (line, i) <- split_lines(content).iterator.zipWithIndex } |
26 for { (line, i) <- split_lines(content).iterator.zipWithIndex } { |
29 { |
|
30 try { |
27 try { |
31 Symbol.decode_strict(line) |
28 Symbol.decode_strict(line) |
32 |
29 |
33 for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) } |
30 for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) } { |
34 { |
|
35 Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) + |
31 Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) + |
36 Position.here(line_pos(i))) |
32 Position.here(line_pos(i))) |
37 } |
33 } |
38 } |
34 } |
39 catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) } |
35 catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) } |
47 |
43 |
48 if (Word.bidi_detect(content)) |
44 if (Word.bidi_detect(content)) |
49 Output.warning("Bidirectional Unicode text" + Position.here(file_pos)) |
45 Output.warning("Bidirectional Unicode text" + Position.here(file_pos)) |
50 } |
46 } |
51 |
47 |
52 def check_hg(root: Path): Unit = |
48 def check_hg(root: Path): Unit = { |
53 { |
|
54 Output.writeln("Checking " + root + " ...") |
49 Output.writeln("Checking " + root + " ...") |
55 val hg = Mercurial.repository(root) |
50 val hg = Mercurial.repository(root) |
56 for { |
51 for { |
57 file <- hg.known_files() |
52 file <- hg.known_files() |
58 if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
53 if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
62 |
57 |
63 /* Isabelle tool wrapper */ |
58 /* Isabelle tool wrapper */ |
64 |
59 |
65 val isabelle_tool = |
60 val isabelle_tool = |
66 Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", |
61 Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", |
67 Scala_Project.here, args => |
62 Scala_Project.here, args => { |
68 { |
|
69 val getopts = Getopts(""" |
63 val getopts = Getopts(""" |
70 Usage: isabelle check_sources [ROOT_DIRS...] |
64 Usage: isabelle check_sources [ROOT_DIRS...] |
71 |
65 |
72 Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS. |
66 Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS. |
73 """) |
67 """) |