src/Pure/General/mercurial.scala
author wenzelm
Sat, 22 Oct 2016 19:57:56 +0200
changeset 64348 4c253e84ae62
parent 64347 602483aa7818
child 64408 50bcf976f276
permissions -rw-r--r--
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);
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
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    13
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    14
object Mercurial
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    15
{
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    16
  /* command-line syntax */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    17
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    18
  def optional(s: String, prefix: String = ""): String =
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64280
diff changeset
    19
    if (s == "") "" else " " + prefix + " " + Bash.string(s)
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    20
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    21
  def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    22
  def opt_rev(s: String): String = optional(s, "--rev")
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    23
  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
    24
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    25
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    26
  /* repository access */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    27
64330
d9a9ae3956f6 more operations;
wenzelm
parents: 64304
diff changeset
    28
  def is_repository(root: Path, ssh: Option[SSH.Session] = None): Boolean =
d9a9ae3956f6 more operations;
wenzelm
parents: 64304
diff changeset
    29
    new Repository(root, ssh).command("root").ok
d9a9ae3956f6 more operations;
wenzelm
parents: 64304
diff changeset
    30
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    31
  def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    32
  {
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    33
    val hg = new Repository(root, ssh)
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    34
    hg.command("root").check
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    35
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    36
  }
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    37
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    38
  def clone_repository(
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    39
    source: String, root: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    40
  {
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    41
    val hg = new Repository(root, ssh)
64255
a9f540881611 more robust;
wenzelm
parents: 64252
diff changeset
    42
    ssh match {
a9f540881611 more robust;
wenzelm
parents: 64252
diff changeset
    43
      case None => Isabelle_System.mkdirs(hg.root.dir)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64255
diff changeset
    44
      case Some(ssh) => ssh.mkdirs(hg.root.dir)
64255
a9f540881611 more robust;
wenzelm
parents: 64252
diff changeset
    45
    }
64304
96bc94c87a81 clarified modules;
wenzelm
parents: 64280
diff changeset
    46
    hg.command("clone", Bash.string(source) + " " + File.bash_path(hg.root), options).check
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    47
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    48
  }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    49
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    50
  def setup_repository(source: String, root: Path, ssh: Option[SSH.Session] = None): Repository =
64252
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    51
  {
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    52
    val present =
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    53
      ssh match {
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    54
        case None => root.is_dir
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64255
diff changeset
    55
        case Some(ssh) => ssh.is_dir(root)
64252
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    56
      }
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    57
    if (present) { val hg = repository(root, ssh = ssh); hg.pull(); hg }
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    58
    else clone_repository(source, root, options = "--noupdate", ssh = ssh)
e84cba30d7ff clarified setup_repository: more uniform pull vs. clone, without update;
wenzelm
parents: 64233
diff changeset
    59
  }
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    60
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    61
  class Repository private[Mercurial](root_path: Path, ssh: Option[SSH.Session])
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    62
  {
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    63
    hg =>
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    64
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    65
    val root =
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    66
      ssh match {
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    67
        case None => root_path.expand
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64255
diff changeset
    68
        case Some(ssh) => root_path.expand_env(ssh.settings)
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    69
      }
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    70
64347
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    71
    def root_url: String =
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    72
      ssh match {
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    73
        case None => root.implode
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    74
        case Some(ssh) => ssh.hg_url + root.implode
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    75
      }
602483aa7818 support for URL notation;
wenzelm
parents: 64330
diff changeset
    76
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    77
    override def toString: String =
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    78
      ssh match {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    79
        case None => root.implode
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64255
diff changeset
    80
        case Some(ssh) => ssh.toString + ":" + root.implode
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    81
      }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    82
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    83
    def command(name: String, args: String = "", options: String = ""): Process_Result =
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    84
    {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    85
      val cmdline =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    86
        "\"${HG:-hg}\"" +
64230
13a97c1d7d22 added setup_repository;
wenzelm
parents: 64198
diff changeset
    87
          (if (name == "clone") "" else " --repository " + File.bash_path(root)) +
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    88
          " --noninteractive " + name + " " + options + " " + args
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    89
      ssh match {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    90
        case None => Isabelle_System.bash(cmdline)
64256
c3197aeae90b simplified SSH.Session: sftp channel is always open and its operations provided by the main interface;
wenzelm
parents: 64255
diff changeset
    91
        case Some(ssh) => ssh.execute(cmdline)
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    92
      }
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    93
    }
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    94
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    95
    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    96
      hg.command("heads", opt_template(template), options).check.out_lines
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    97
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64230
diff changeset
    98
    def identify(rev: String = "tip", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    99
      hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
   100
64232
367d83d6030e clarified hg.id operation, with explicit tip as default;
wenzelm
parents: 64230
diff changeset
   101
    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
   102
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
   103
    def manifest(rev: String = "", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   104
      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
   105
64033
2989c1f2593a tuned signature;
wenzelm
parents: 64028
diff changeset
   106
    def log(rev: String = "", template: String = "", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   107
      hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
64027
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
   108
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
   109
    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
   110
    {
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
   111
      hg.command("push", opt_rev(rev) + opt_flag("--force", force) + optional(remote), options).
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
   112
        check
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
   113
    }
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
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   115
    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   116
      hg.command("pull", opt_rev(rev) + optional(remote), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   117
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   118
    def update(
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   119
      rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   120
    {
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   121
      hg.command("update",
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
   122
        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
   123
    }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
   124
  }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
   125
}