1/*  Title:      Pure/Admin/check_sources.scala
2    Author:     Makarius
3
4Some sanity checks for Isabelle sources.
5*/
6
7package isabelle
8
9
10object Check_Sources
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    if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
19      Output.warning("Illegal file-name on Windows" + Position.here(file_pos))
20
21    val content = File.read(path)
22
23    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
24    {
25      try {
26        Symbol.decode_strict(line)
27
28        for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
29        {
30          Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
31            Position.here(line_pos(i)))
32        }
33      }
34      catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
35
36      if (line.contains('\t'))
37        Output.warning("TAB character" + Position.here(line_pos(i)))
38    }
39
40    if (content.contains('\r'))
41      Output.warning("CR character" + Position.here(file_pos))
42
43    if (Word.bidi_detect(content))
44      Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
45  }
46
47  def check_hg(root: Path)
48  {
49    Output.writeln("Checking " + root + " ...")
50    val hg = Mercurial.repository(root)
51    for {
52      file <- hg.known_files()
53      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
54    } check_file(root + Path.explode(file))
55  }
56
57
58  /* Isabelle tool wrapper */
59
60  val isabelle_tool =
61    Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
62    {
63      val getopts = Getopts("""
64Usage: isabelle check_sources [ROOT_DIRS...]
65
66  Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
67""")
68
69      val specs = getopts(args)
70      if (specs.isEmpty) getopts.usage()
71
72      for (root <- specs) check_hg(Path.explode(root))
73    })
74}
75