proper tool wrap-up;
authorwenzelm
Fri, 02 May 2014 19:30:34 +0200
changeset 56829 f151ade98b15
parent 56828 08041569357e
child 56830 e760242101fc
proper tool wrap-up;
Admin/Release/CHECKLIST
src/Pure/Tools/check_source.scala
--- a/Admin/Release/CHECKLIST	Fri May 02 19:28:32 2014 +0200
+++ b/Admin/Release/CHECKLIST	Fri May 02 19:30:34 2014 +0200
@@ -17,7 +17,8 @@
 
 - check HTML header of library;
 
-- check sources: see isabelle.Check_Source;
+- check sources:
+    isabelle java isabelle.Check_Source '~~' '$AFP_BASE'
 
 - run isabelle update_keywords;
 
--- a/src/Pure/Tools/check_source.scala	Fri May 02 19:28:32 2014 +0200
+++ b/src/Pure/Tools/check_source.scala	Fri May 02 19:30:34 2014 +0200
@@ -37,5 +37,25 @@
     if (content.contains('\r'))
       Output.warning("CR character" + Position.here(file_pos))
   }
+
+  def check_hg(root: Path)
+  {
+    System.err.println("Checking " + root + " ...")
+    Isabelle_System.hg("--repository " + Isabelle_System.shell_path(root) + " root").check_error
+    for {
+      file <- Isabelle_System.hg("manifest", root).check_error.out_lines
+      if file.endsWith(".thy") || file.endsWith(".ML")
+    } 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))
+    }
+  }
 }