author | wenzelm |
Mon, 01 Mar 2021 22:22:12 +0100 | |
changeset 73340 | 0ffcad1f6130 |
parent 72763 | 3cc73d00553c |
child 75393 | 87ebf5a50283 |
permissions | -rw-r--r-- |
64161 | 1 |
/* Title: Pure/Admin/check_sources.scala |
56791 | 2 |
Author: Makarius |
3 |
||
4 |
Some sanity checks for Isabelle sources. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
62452 | 10 |
object Check_Sources |
56791 | 11 |
{ |
73340 | 12 |
def check_file(path: Path): Unit = |
56791 | 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 |
||
69367 | 18 |
if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux")) |
64324
416f4d031afd
check Windows file names, e.g. relavant for native Mercurial, but also for Isabelle/Scala;
wenzelm
parents:
64162
diff
changeset
|
19 |
Output.warning("Illegal file-name on Windows" + Position.here(file_pos)) |
416f4d031afd
check Windows file names, e.g. relavant for native Mercurial, but also for Isabelle/Scala;
wenzelm
parents:
64162
diff
changeset
|
20 |
|
72254 | 21 |
val bytes = Bytes.read(path) |
22 |
val content = bytes.text |
|
23 |
||
24 |
if (Bytes(content) != bytes) { |
|
25 |
Output.warning("Bad UTF8 encoding" + Position.here(file_pos)) |
|
26 |
} |
|
56791 | 27 |
|
28 |
for { (line, i) <- split_lines(content).iterator.zipWithIndex } |
|
29 |
{ |
|
30 |
try { |
|
31 |
Symbol.decode_strict(line) |
|
32 |
||
64610 | 33 |
for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) } |
56791 | 34 |
{ |
64610 | 35 |
Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) + |
56791 | 36 |
Position.here(line_pos(i))) |
37 |
} |
|
38 |
} |
|
62814 | 39 |
catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) } |
56791 | 40 |
|
41 |
if (line.contains('\t')) |
|
56792 | 42 |
Output.warning("TAB character" + Position.here(line_pos(i))) |
56791 | 43 |
} |
44 |
||
45 |
if (content.contains('\r')) |
|
56792 | 46 |
Output.warning("CR character" + Position.here(file_pos)) |
62814 | 47 |
|
48 |
if (Word.bidi_detect(content)) |
|
64368 | 49 |
Output.warning("Bidirectional Unicode text" + Position.here(file_pos)) |
56791 | 50 |
} |
56829 | 51 |
|
73340 | 52 |
def check_hg(root: Path): Unit = |
56829 | 53 |
{ |
56830
e760242101fc
tuned signature -- channels for diagnostic output for system tools means stderr;
wenzelm
parents:
56829
diff
changeset
|
54 |
Output.writeln("Checking " + root + " ...") |
64162 | 55 |
val hg = Mercurial.repository(root) |
56 |
for { |
|
65822
17b8528c2f53
clarified notion of known files (before actual commit);
wenzelm
parents:
64610
diff
changeset
|
57 |
file <- hg.known_files() |
64162 | 58 |
if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT") |
59 |
} check_file(root + Path.explode(file)) |
|
56829 | 60 |
} |
61 |
||
62 |
||
62834 | 63 |
/* Isabelle tool wrapper */ |
56829 | 64 |
|
62834 | 65 |
val isabelle_tool = |
72763 | 66 |
Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", |
67 |
Scala_Project.here, args => |
|
62834 | 68 |
{ |
62454 | 69 |
val getopts = Getopts(""" |
62452 | 70 |
Usage: isabelle check_sources [ROOT_DIRS...] |
71 |
||
65822
17b8528c2f53
clarified notion of known files (before actual commit);
wenzelm
parents:
64610
diff
changeset
|
72 |
Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS. |
62452 | 73 |
""") |
74 |
||
75 |
val specs = getopts(args) |
|
76 |
if (specs.isEmpty) getopts.usage() |
|
77 |
||
78 |
for (root <- specs) check_hg(Path.explode(root)) |
|
69277
258bef08b31e
support for user-defined Isabelle/Scala command-line tools;
wenzelm
parents:
65822
diff
changeset
|
79 |
}) |
56791 | 80 |
} |