src/Pure/Admin/check_sources.scala
author wenzelm
Tue Oct 18 10:05:38 2016 +0200 (2016-10-18)
changeset 64294 303976a45afe
parent 64162 03057a8fdd1f
child 64324 416f4d031afd
permissions -rw-r--r--
shared_home is default for classic isatest home setup;
distinct ISABELLE_IDENTIFIER for all tasks;
     1 /*  Title:      Pure/Admin/check_sources.scala
     2     Author:     Makarius
     3 
     4 Some sanity checks for Isabelle sources.
     5 */
     6 
     7 package isabelle
     8 
     9 
    10 object 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     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.warning(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     if (Word.bidi_detect(content))
    41       Output.warning("Bidirectional Unicode text " + Position.here(file_pos))
    42   }
    43 
    44   def check_hg(root: Path)
    45   {
    46     Output.writeln("Checking " + root + " ...")
    47     val hg = Mercurial.repository(root)
    48     for {
    49       file <- hg.manifest()
    50       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    51     } check_file(root + Path.explode(file))
    52   }
    53 
    54 
    55   /* Isabelle tool wrapper */
    56 
    57   val isabelle_tool =
    58     Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources", args =>
    59     {
    60       val getopts = Getopts("""
    61 Usage: isabelle check_sources [ROOT_DIRS...]
    62 
    63   Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
    64 """)
    65 
    66       val specs = getopts(args)
    67       if (specs.isEmpty) getopts.usage()
    68 
    69       for (root <- specs) check_hg(Path.explode(root))
    70     }, admin = true)
    71 }