src/Pure/Tools/check_source.scala
author wenzelm
Thu Aug 20 19:15:17 2015 +0200 (2015-08-20)
changeset 60988 1d7a7e33fd67
parent 56830 e760242101fc
child 62226 9f7293af6fb8
permissions -rw-r--r--
tuned signature, according to ML version;
     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_error
    45     for {
    46       file <- Isabelle_System.hg("manifest", root).check_error.out_lines
    47       if file.endsWith(".thy") || file.endsWith(".ML")
    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