src/Pure/Admin/check_sources.scala
changeset 75393 87ebf5a50283
parent 73340 0ffcad1f6130
child 75394 42267c650205
equal deleted inserted replaced
75388:b3ca4a6ed74b 75393:87ebf5a50283
     5 */
     5 */
     6 
     6 
     7 package isabelle
     7 package isabelle
     8 
     8 
     9 
     9 
    10 object Check_Sources
    10 object Check_Sources {
    11 {
    11   def check_file(path: Path): Unit = {
    12   def check_file(path: Path): Unit =
       
    13   {
       
    14     val file_name = path.implode
    12     val file_name = path.implode
    15     val file_pos = path.position
    13     val file_pos = path.position
    16     def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
    14     def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
    17 
    15 
    18     if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
    16     if (space_explode('/', Word.lowercase(path.expand.drop_ext.implode)).contains("aux"))
    23 
    21 
    24     if (Bytes(content) != bytes) {
    22     if (Bytes(content) != bytes) {
    25       Output.warning("Bad UTF8 encoding" + Position.here(file_pos))
    23       Output.warning("Bad UTF8 encoding" + Position.here(file_pos))
    26     }
    24     }
    27 
    25 
    28     for { (line, i) <- split_lines(content).iterator.zipWithIndex }
    26     for { (line, i) <- split_lines(content).iterator.zipWithIndex } {
    29     {
       
    30       try {
    27       try {
    31         Symbol.decode_strict(line)
    28         Symbol.decode_strict(line)
    32 
    29 
    33         for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) }
    30         for { c <- Codepoint.iterator(line); if c > 128 && !Character.isAlphabetic(c) } {
    34         {
       
    35           Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
    31           Output.warning("Suspicious Unicode character " + quote(Codepoint.string(c)) +
    36             Position.here(line_pos(i)))
    32             Position.here(line_pos(i)))
    37         }
    33         }
    38       }
    34       }
    39       catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
    35       catch { case ERROR(msg) => Output.warning(msg + Position.here(line_pos(i))) }
    47 
    43 
    48     if (Word.bidi_detect(content))
    44     if (Word.bidi_detect(content))
    49       Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
    45       Output.warning("Bidirectional Unicode text" + Position.here(file_pos))
    50   }
    46   }
    51 
    47 
    52   def check_hg(root: Path): Unit =
    48   def check_hg(root: Path): Unit = {
    53   {
       
    54     Output.writeln("Checking " + root + " ...")
    49     Output.writeln("Checking " + root + " ...")
    55     val hg = Mercurial.repository(root)
    50     val hg = Mercurial.repository(root)
    56     for {
    51     for {
    57       file <- hg.known_files()
    52       file <- hg.known_files()
    58       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    53       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
    62 
    57 
    63   /* Isabelle tool wrapper */
    58   /* Isabelle tool wrapper */
    64 
    59 
    65   val isabelle_tool =
    60   val isabelle_tool =
    66     Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources",
    61     Isabelle_Tool("check_sources", "some sanity checks for Isabelle sources",
    67       Scala_Project.here, args =>
    62       Scala_Project.here, args => {
    68     {
       
    69       val getopts = Getopts("""
    63       val getopts = Getopts("""
    70 Usage: isabelle check_sources [ROOT_DIRS...]
    64 Usage: isabelle check_sources [ROOT_DIRS...]
    71 
    65 
    72   Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
    66   Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
    73 """)
    67 """)