src/Pure/Tools/check_source.scala
author wenzelm
Mon Dec 22 16:44:24 2014 +0100 (2014-12-22 ago)
changeset 59175 bf465f335e85
parent 56830 e760242101fc
child 60988 1d7a7e33fd67
permissions -rw-r--r--
system option "pretty_margin" is superseded by "thy_output_margin";
wenzelm@56791
     1
/*  Title:      Pure/Tools/check_source.scala
wenzelm@56791
     2
    Author:     Makarius
wenzelm@56791
     3
wenzelm@56791
     4
Some sanity checks for Isabelle sources.
wenzelm@56791
     5
*/
wenzelm@56791
     6
wenzelm@56791
     7
package isabelle
wenzelm@56791
     8
wenzelm@56791
     9
wenzelm@56791
    10
object Check_Source
wenzelm@56791
    11
{
wenzelm@56791
    12
  def check_file(path: Path)
wenzelm@56791
    13
  {
wenzelm@56791
    14
    val file_name = path.implode
wenzelm@56791
    15
    val file_pos = path.position
wenzelm@56791
    16
    def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
wenzelm@56791
    17
wenzelm@56791
    18
    val content = File.read(path)
wenzelm@56791
    19
wenzelm@56791
    20
    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
wenzelm@56791
    21
    {
wenzelm@56791
    22
      try {
wenzelm@56791
    23
        Symbol.decode_strict(line)
wenzelm@56791
    24
wenzelm@56791
    25
        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
wenzelm@56791
    26
        {
wenzelm@56792
    27
          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
wenzelm@56791
    28
            Position.here(line_pos(i)))
wenzelm@56791
    29
        }
wenzelm@56791
    30
      }
wenzelm@56791
    31
      catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
wenzelm@56791
    32
wenzelm@56791
    33
      if (line.contains('\t'))
wenzelm@56792
    34
        Output.warning("TAB character" + Position.here(line_pos(i)))
wenzelm@56791
    35
    }
wenzelm@56791
    36
wenzelm@56791
    37
    if (content.contains('\r'))
wenzelm@56792
    38
      Output.warning("CR character" + Position.here(file_pos))
wenzelm@56791
    39
  }
wenzelm@56829
    40
wenzelm@56829
    41
  def check_hg(root: Path)
wenzelm@56829
    42
  {
wenzelm@56830
    43
    Output.writeln("Checking " + root + " ...")
wenzelm@56829
    44
    Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
wenzelm@56829
    45
    for {
wenzelm@56829
    46
      file <- Isabelle_System.hg("manifest", root).check_error.out_lines
wenzelm@56829
    47
      if file.endsWith(".thy") || file.endsWith(".ML")
wenzelm@56829
    48
    } check_file(root + Path.explode(file))
wenzelm@56829
    49
  }
wenzelm@56829
    50
wenzelm@56829
    51
wenzelm@56829
    52
  /* command line entry point */
wenzelm@56829
    53
wenzelm@56829
    54
  def main(args: Array[String])
wenzelm@56829
    55
  {
wenzelm@56829
    56
    Command_Line.tool0 {
wenzelm@56829
    57
      for (root <- args) check_hg(Path.explode(root))
wenzelm@56829
    58
    }
wenzelm@56829
    59
  }
wenzelm@56791
    60
}
wenzelm@56791
    61