--- 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)
--- 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