src/Pure/General/mercurial.scala
author wenzelm
Mon, 13 Nov 2017 14:31:25 +0100
changeset 67066 1645cef7a49c
parent 67065 d9a347af82ab
child 67068 46ce32fd5f53
permissions -rw-r--r--
proper ssh.bash_path;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/mercurial.scala
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     3
64280
wenzelm
parents: 64256
diff changeset
     4
Support for Mercurial repositories, with local or remote repository clone
wenzelm
parents: 64256
diff changeset
     5
and working directory (via ssh connection).
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     6
*/
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     7
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     8
package isabelle
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     9
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    10
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    11
import java.io.{File => JFile}
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    12
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
    13
import scala.annotation.tailrec
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
    14
import scala.collection.mutable
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
    15
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    16
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    17
object Mercurial
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    18
{
66895
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66570
diff changeset
    19
  type Graph = isabelle.Graph[String, Unit]
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66570
diff changeset
    20
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66570
diff changeset
    21
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    22
  /* command-line syntax */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    23
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    24
  def optional(s: String, prefix: String = ""): String =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64280
diff changeset
    25
    if (s == "") "" else " " + prefix + " " + Bash.string(s)
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    26
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    27
  def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    28
  def opt_rev(s: String): String = optional(s, "--rev")
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    29
  def opt_template(s: String): String = optional(s, "--template")
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    30
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    31
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    32
  /* repository access */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    33
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    34
  def is_repository(root: Path, ssh: SSH.System = SSH.Local): Boolean =
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    35
    ssh.is_dir(root + Path.explode(".hg")) &&
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    36
    new Repository(root, ssh).command("root").ok
64330
d9a9ae3956f6 more operations;
wenzelm
parents: 64304
diff changeset
    37
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    38
  def repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    39
  {
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    40
    val hg = new Repository(root, ssh)
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    41
    hg.command("root").check
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    42
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    43
  }
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    44
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    45
  def find_repository(start: Path, ssh: SSH.System = SSH.Local): Option[Repository] =
65559
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    46
  {
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    47
    def find(root: Path): Option[Repository] =
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    48
      if (is_repository(root, ssh)) Some(repository(root, ssh = ssh))
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    49
      else if (root.is_root) None
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    50
      else find(root + Path.parent)
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    51
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    52
    find(ssh.expand_path(start))
65559
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    53
  }
7ff7781913a4 more operations;
wenzelm
parents: 64505
diff changeset
    54
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    55
  private def make_repository(root: Path, cmd: String, args: String, ssh: SSH.System = SSH.Local)
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    56
    : Repository =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    57
  {
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    58
    val hg = new Repository(root, ssh)
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    59
    ssh.mkdirs(hg.root.dir)
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    60
    hg.command(cmd, args, repository = false).check
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    61
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    62
  }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    63
67065
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    64
  def init_repository(root: Path, ssh: SSH.System = SSH.Local): Repository =
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    65
    make_repository(root, "init", ssh.bash_path(root), ssh = ssh)
67065
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    66
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    67
  def clone_repository(source: String, root: Path,
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    68
      rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    69
    make_repository(root, "clone",
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    70
      options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
67065
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    71
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    72
  def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
64252
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    73
  {
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    74
    if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
66105
8889aad1ff92 reverted 94cad7590015: does not help much on Windows;
wenzelm
parents: 66104
diff changeset
    75
    else clone_repository(source, root, options = "--noupdate", ssh = ssh)
64252
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    76
  }
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    77
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    78
  class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    79
  {
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    80
    hg =>
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    81
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    82
    val root = ssh.expand_path(root_path)
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    83
    def root_url: String = ssh.hg_url + root.implode
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    84
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    85
    override def toString: String = ssh.prefix + root.implode
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    86
67065
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    87
    def command(name: String, args: String = "", options: String = "",
d9a347af82ab more operations;
wenzelm
parents: 66895
diff changeset
    88
      repository: Boolean = true): Process_Result =
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    89
    {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    90
      val cmdline =
65825
11f87ab51ddb more robust command invocation, without defaults from hgrc;
wenzelm
parents: 65822
diff changeset
    91
        "\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
67066
1645cef7a49c proper ssh.bash_path;
wenzelm
parents: 67065
diff changeset
    92
          (if (repository) " --repository " + ssh.bash_path(root) else "") +
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    93
          " --noninteractive " + name + " " + options + " " + args
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
    94
      ssh.execute(cmdline)
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    95
    }
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    96
64505
545a7ab3c35f optional component setup;
wenzelm
parents: 64451
diff changeset
    97
    def archive(target: String, rev: String = "", options: String = ""): Unit =
545a7ab3c35f optional component setup;
wenzelm
parents: 64451
diff changeset
    98
      hg.command("archive", opt_rev(rev) + " " + Bash.string(target), options).check
545a7ab3c35f optional component setup;
wenzelm
parents: 64451
diff changeset
    99
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   100
    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   101
      hg.command("heads", opt_template(template), options).check.out_lines
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   102
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64230
diff changeset
   103
    def identify(rev: String = "tip", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   104
      hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
   105
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64230
diff changeset
   106
    def id(rev: String = "tip"): String = identify(rev, options = "-i")
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64230
diff changeset
   107
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
   108
    def manifest(rev: String = "", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   109
      hg.command("manifest", opt_rev(rev), options).check.out_lines
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
   110
64033
2989c1f2593a tuned signature;
wenzelm
parents: 64028
diff changeset
   111
    def log(rev: String = "", template: String = "", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   112
      hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
64027
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
   113
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64347
diff changeset
   114
    def push(remote: String = "", rev: String = "", force: Boolean = false, options: String = "")
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64347
diff changeset
   115
    {
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64347
diff changeset
   116
      hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
64408
50bcf976f276 clarified hg push return code: 1 means "nothing to push";
wenzelm
parents: 64348
diff changeset
   117
        check_rc(rc => rc == 0 | rc == 1)
64348
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64347
diff changeset
   118
    }
4c253e84ae62 clarified push/pull chain: current ISABELLE_HOME may server as source for changes that are not published on isabelle_repos_source yet (e.g. isabelle-release branch);
wenzelm
parents: 64347
diff changeset
   119
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   120
    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   121
      hg.command("pull", opt_rev(rev) + optional(remote), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   122
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   123
    def update(
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   124
      rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   125
    {
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   126
      hg.command("update",
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   127
        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   128
    }
65819
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   129
65822
17b8528c2f53 clarified notion of known files (before actual commit);
wenzelm
parents: 65819
diff changeset
   130
    def known_files(): List[String] =
65825
11f87ab51ddb more robust command invocation, without defaults from hgrc;
wenzelm
parents: 65822
diff changeset
   131
      hg.command("status", options = "--modified --added --clean --no-status").check.out_lines
65819
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   132
66895
e378e0468ef2 tuned: build hg_graph only once;
wenzelm
parents: 66570
diff changeset
   133
    def graph(): Graph =
65819
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   134
    {
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   135
      val Node = """^node: (\w{12}) (\w{12}) (\w{12})""".r
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   136
      val log_result =
65825
11f87ab51ddb more robust command invocation, without defaults from hgrc;
wenzelm
parents: 65822
diff changeset
   137
        log(template = """node: {node|short} {p1node|short} {p2node|short}\n""")
65819
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   138
      (Graph.string[Unit] /: split_lines(log_result)) {
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   139
        case (graph, Node(x, y, z)) =>
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   140
          val deps = List(y, z).filterNot(s => s.forall(_ == '0'))
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   141
          val graph1 = (graph /: (x :: deps))(_.default_node(_, ()))
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   142
          (graph1 /: deps)({ case (g, dep) => g.add_edge(dep, x) })
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   143
        case (graph, _) => graph
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   144
      }
ff3dc9325eaa explore repository structure, with minimal assumptions about "hg log" output;
wenzelm
parents: 65818
diff changeset
   145
    }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
   146
  }
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   147
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   148
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   149
  /* unknown files */
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   150
66570
9af879e222cc clarified signature;
wenzelm
parents: 66569
diff changeset
   151
  def unknown_files(files: List[Path], ssh: SSH.System = SSH.Local): List[Path] =
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   152
  {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   153
    val unknown = new mutable.ListBuffer[Path]
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   154
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   155
    @tailrec def check(paths: List[Path])
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   156
    {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   157
      paths match {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   158
        case path :: rest =>
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   159
          find_repository(path, ssh) match {
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   160
            case None => unknown += path; check(rest)
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   161
            case Some(hg) =>
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   162
              val known =
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   163
                hg.known_files().iterator.map(name =>
65833
95fd3b9888e6 tuned signature;
wenzelm
parents: 65832
diff changeset
   164
                  (hg.root + Path.explode(name)).canonical_file).toSet
95fd3b9888e6 tuned signature;
wenzelm
parents: 65832
diff changeset
   165
              if (!known(path.canonical_file)) unknown += path
95fd3b9888e6 tuned signature;
wenzelm
parents: 65832
diff changeset
   166
              check(rest.filterNot(p => known(p.canonical_file)))
65832
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   167
          }
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   168
        case Nil =>
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   169
      }
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   170
    }
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   171
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   172
    check(files)
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   173
    unknown.toList
2fb85623c386 implicitly check for unknown files (not part of a Mercurial repository);
wenzelm
parents: 65825
diff changeset
   174
  }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
   175
}