# HG changeset patch
# User wenzelm
# Date 1494768860 -7200
# Node ID 17b8528c2f533c4af93e1ca11ea1d07f81b61319
# Parent  89c1f40656e5e364fc42b8ff0610c7baab89a666
clarified notion of known files (before actual commit);

diff -r 89c1f40656e5 -r 17b8528c2f53 src/Pure/Admin/check_sources.scala
--- a/src/Pure/Admin/check_sources.scala	Sun May 14 15:16:38 2017 +0200
+++ b/src/Pure/Admin/check_sources.scala	Sun May 14 15:34:20 2017 +0200
@@ -49,7 +49,7 @@
     Output.writeln("Checking " + root + " ...")
     val hg = Mercurial.repository(root)
     for {
-      file <- hg.manifest()
+      file <- hg.known_files()
       if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
     } check_file(root + Path.explode(file))
   }
@@ -63,7 +63,7 @@
       val getopts = Getopts("""
 Usage: isabelle check_sources [ROOT_DIRS...]
 
-  Check .thy, .ML, ROOT files from manifest of Mercurial ROOT_DIRS.
+  Check .thy, .ML, ROOT against known files of Mercurial ROOT_DIRS.
 """)
 
       val specs = getopts(args)
diff -r 89c1f40656e5 -r 17b8528c2f53 src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Sun May 14 15:16:38 2017 +0200
+++ b/src/Pure/General/mercurial.scala	Sun May 14 15:34:20 2017 +0200
@@ -138,6 +138,10 @@
         opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
     }
 
+    def known_files(): List[String] =
+      hg.command("status", options = "--modified --added --clean --no-status --color=never").
+        check.out_lines
+
     def length(): Int =
       identify(options = "-n") match {
         case Value.Int(n) => n + 1