# HG changeset patch
# User wenzelm
# Date 1456671423 -3600
# Node ID f25b67245699a1da4e0a8a4089f0301c84f03f53
# Parent  040b94ffbddebeac3d268d22d3a18a5015c94914
more official "isabelle check_sources";

diff -r 040b94ffbdde -r f25b67245699 Admin/Release/CHECKLIST
--- a/Admin/Release/CHECKLIST	Sun Feb 28 15:43:56 2016 +0100
+++ b/Admin/Release/CHECKLIST	Sun Feb 28 15:57:03 2016 +0100
@@ -12,7 +12,7 @@
 - test "#!/usr/bin/env isabelle_scala_script";
 
 - check sources:
-    isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
+    isabelle check_sources '~~' '$AFP_BASE'
 
 - check ANNOUNCE, README, NEWS, COPYRIGHT, CONTRIBUTORS;
 
diff -r 040b94ffbdde -r f25b67245699 Admin/lib/Tools/check_sources
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/lib/Tools/check_sources	Sun Feb 28 15:57:03 2016 +0100
@@ -0,0 +1,9 @@
+#!/usr/bin/env bash
+#
+# Author: Makarius
+#
+# DESCRIPTION: some sanity checks for Isabelle sources
+
+isabelle_admin_build jars || exit $?
+
+"$ISABELLE_TOOL" java isabelle.Check_Sources "$@"
diff -r 040b94ffbdde -r f25b67245699 src/Pure/Tools/check_source.scala
--- a/src/Pure/Tools/check_source.scala	Sun Feb 28 15:43:56 2016 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,61 +0,0 @@
-/*  Title:      Pure/Tools/check_source.scala
-    Author:     Makarius
-
-Some sanity checks for Isabelle sources.
-*/
-
-package isabelle
-
-
-object Check_Source
-{
-  def check_file(path: Path)
-  {
-    val file_name = path.implode
-    val file_pos = path.position
-    def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
-
-    val content = File.read(path)
-
-    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
-    {
-      try {
-        Symbol.decode_strict(line)
-
-        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
-        {
-          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
-            Position.here(line_pos(i)))
-        }
-      }
-      catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
-
-      if (line.contains('\t'))
-        Output.warning("TAB character" + Position.here(line_pos(i)))
-    }
-
-    if (content.contains('\r'))
-      Output.warning("CR character" + Position.here(file_pos))
-  }
-
-  def check_hg(root: Path)
-  {
-    Output.writeln("Checking " + root + " ...")
-    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
-    for {
-      file <- Isabelle_System.hg("manifest", root).check.out_lines
-      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
-    } check_file(root + Path.explode(file))
-  }
-
-
-  /* command line entry point */
-
-  def main(args: Array[String])
-  {
-    Command_Line.tool0 {
-      for (root <- args) check_hg(Path.explode(root))
-    }
-  }
-}
-
diff -r 040b94ffbdde -r f25b67245699 src/Pure/Tools/check_sources.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Tools/check_sources.scala	Sun Feb 28 15:57:03 2016 +0100
@@ -0,0 +1,69 @@
+/*  Title:      Pure/Tools/check_sources.scala
+    Author:     Makarius
+
+Some sanity checks for Isabelle sources.
+*/
+
+package isabelle
+
+
+object Check_Sources
+{
+  def check_file(path: Path)
+  {
+    val file_name = path.implode
+    val file_pos = path.position
+    def line_pos(i: Int) = Position.Line_File(i + 1, file_name)
+
+    val content = File.read(path)
+
+    for { (line, i) <- split_lines(content).iterator.zipWithIndex }
+    {
+      try {
+        Symbol.decode_strict(line)
+
+        for { c <- Word.codepoint_iterator(line); if c > 128 && !Character.isAlphabetic(c) }
+        {
+          Output.warning("Suspicious Unicode character " + quote(Word.codepoint(c)) +
+            Position.here(line_pos(i)))
+        }
+      }
+      catch { case ERROR(msg) => Output.error_message(msg + Position.here(line_pos(i))) }
+
+      if (line.contains('\t'))
+        Output.warning("TAB character" + Position.here(line_pos(i)))
+    }
+
+    if (content.contains('\r'))
+      Output.warning("CR character" + Position.here(file_pos))
+  }
+
+  def check_hg(root: Path)
+  {
+    Output.writeln("Checking " + root + " ...")
+    Isabelle_System.hg("--repository " + File.shell_path(root) + " root").check
+    for {
+      file <- Isabelle_System.hg("manifest", root).check.out_lines
+      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+    } check_file(root + Path.explode(file))
+  }
+
+
+  /* command line entry point */
+
+  def main(args: Array[String])
+  {
+    Command_Line.tool0 {
+      val getopts = Getopts(() => """
+Usage: isabelle check_sources [ROOT_DIRS...]
+
+  Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
+""")
+
+      val specs = getopts(args)
+      if (specs.isEmpty) getopts.usage()
+
+      for (root <- specs) check_hg(Path.explode(root))
+    }
+  }
+}
diff -r 040b94ffbdde -r f25b67245699 src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Feb 28 15:43:56 2016 +0100
+++ b/src/Pure/build-jars	Sun Feb 28 15:57:03 2016 +0100
@@ -97,7 +97,7 @@
   Tools/build_console.scala
   Tools/build_doc.scala
   Tools/check_keywords.scala
-  Tools/check_source.scala
+  Tools/check_sources.scala
   Tools/debugger.scala
   Tools/doc.scala
   Tools/main.scala