# HG changeset patch
# User wenzelm
# Date 1475430438 -7200
# Node ID e11ccb5aa82f93a8c7547a9fcfe5e282cd0c7711
# Parent  3f47fec9edfc000ff0a452e9e5f11dee95a1e045
more formal Mercurial support (with the potential to upgrade to command server);

diff -r 3f47fec9edfc -r e11ccb5aa82f src/Pure/General/mercurial.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/mercurial.scala	Sun Oct 02 19:47:18 2016 +0200
@@ -0,0 +1,38 @@
+/*  Title:      Pure/General/mercurial.scala
+    Author:     Makarius
+
+Support for Mercurial repositories.
+*/
+
+package isabelle
+
+
+import java.io.{File => JFile}
+
+
+object Mercurial
+{
+  /* command-line syntax */
+
+  def opt_rev(rev: String): String = if (rev == "") "" else " --rev " + File.bash_string(rev)
+
+
+  /* repository access */
+
+  def open_repository(root: Path): Repository = new Repository(root)
+
+  class Repository private[Mercurial](val root: Path)
+  {
+    override def toString: String = root.toString
+
+    def close() { }
+
+    def command(cmd: String, cwd: JFile = null): Process_Result =
+      Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd)
+
+    def manifest(rev: String = "", cwd: JFile = null): List[String] =
+      command("manifest" + opt_rev(rev), cwd = cwd).check.out_lines
+
+    command("root").check
+  }
+}
diff -r 3f47fec9edfc -r e11ccb5aa82f src/Pure/Tools/check_sources.scala
--- a/src/Pure/Tools/check_sources.scala	Sun Oct 02 19:36:57 2016 +0200
+++ b/src/Pure/Tools/check_sources.scala	Sun Oct 02 19:47:18 2016 +0200
@@ -44,11 +44,12 @@
   def check_hg(root: Path)
   {
     Output.writeln("Checking " + root + " ...")
-    Isabelle_System.hg("--repository " + File.bash_path(root) + " root").check
-    for {
-      file <- Isabelle_System.hg("manifest", cwd = root.file).check.out_lines
-      if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
-    } check_file(root + Path.explode(file))
+    using(Mercurial.open_repository(root)) { hg =>
+      for {
+        file <- hg.manifest()
+        if file.endsWith(".thy") || file.endsWith(".ML") || file.endsWith("/ROOT")
+      } check_file(root + Path.explode(file))
+    }
   }
 
 
diff -r 3f47fec9edfc -r e11ccb5aa82f src/Pure/build-jars
--- a/src/Pure/build-jars	Sun Oct 02 19:36:57 2016 +0200
+++ b/src/Pure/build-jars	Sun Oct 02 19:47:18 2016 +0200
@@ -36,6 +36,7 @@
   General/json.scala
   General/linear_set.scala
   General/long_name.scala
+  General/mercurial.scala
   General/multi_map.scala
   General/output.scala
   General/path.scala