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