src/Pure/General/mercurial.scala
author wenzelm
Wed, 12 Oct 2016 15:51:20 +0200
changeset 64169 3b618d52119e
parent 64168 e573b985390c
child 64198 351b8211aef9
permissions -rw-r--r--
tuned;
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
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     4
Support for Mercurial repositories.
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     5
*/
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
package isabelle
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
     8
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
import java.io.{File => JFile}
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    11
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
object Mercurial
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    14
{
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    15
  /* command-line syntax */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    16
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    17
  def optional(s: String, prefix: String = ""): String =
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    18
    if (s == "") "" else " " + prefix + " " + File.bash_string(s)
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    19
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    20
  def opt_flag(flag: String, b: Boolean): String = if (b) " " + flag else ""
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    21
  def opt_rev(s: String): String = optional(s, "--rev")
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    22
  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
    23
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
  /* repository access */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    26
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    27
  def repository(root: Path, ssh: Option[SSH.Session] = None): Repository =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    28
  {
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    29
    val hg = new Repository(root, ssh)
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    30
    hg.command("root").check
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    31
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    32
  }
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    33
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    34
  def clone_repository(
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    35
    source: String, dest: Path, options: String = "", ssh: Option[SSH.Session] = None): Repository =
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    36
  {
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    37
    val hg = new Repository(dest, ssh)
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    38
    hg.command("clone",
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    39
      File.bash_string(source) + " " + File.bash_string(dest.implode), options).check
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    40
    hg
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    41
  }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    42
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    43
  class Repository private[Mercurial](val root: Path, ssh: Option[SSH.Session])
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    44
  {
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    45
    hg =>
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    46
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    47
    override def toString: String =
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    48
      ssh match {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    49
        case None => root.implode
64169
wenzelm
parents: 64168
diff changeset
    50
        case Some(session) => session.toString + ":" + root.implode
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    51
      }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    52
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    53
    def command(name: String, args: String = "", options: String = ""): Process_Result =
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    54
    {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    55
      val cmdline =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    56
        "\"${HG:-hg}\"" +
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    57
          (if (name == "clone") "" else " --repository " + File.bash_string(root.implode)) +
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    58
          " --noninteractive " + name + " " + options + " " + args
64167
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    59
      ssh match {
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    60
        case None => Isabelle_System.bash(cmdline)
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    61
        case Some(session) => session.execute(cmdline)
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    62
      }
097d122222f6 support remote repositories via ssh command execution;
wenzelm
parents: 64162
diff changeset
    63
    }
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    64
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    65
    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    66
      hg.command("heads", opt_template(template), options).check.out_lines
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    67
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    68
    def identify(rev: String = "", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    69
      hg.command("id", opt_rev(rev), options).check.out_lines.headOption getOrElse ""
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    70
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    71
    def manifest(rev: String = "", options: String = ""): List[String] =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    72
      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
    73
64033
2989c1f2593a tuned signature;
wenzelm
parents: 64028
diff changeset
    74
    def log(rev: String = "", template: String = "", options: String = ""): String =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    75
      hg.command("log", opt_rev(rev) + opt_template(template), options).check.out
64027
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
    76
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    77
    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    78
      hg.command("pull", opt_rev(rev) + optional(remote), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    79
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    80
    def update(
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    81
      rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    82
    {
64168
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    83
      hg.command("update",
e573b985390c added clone_repository;
wenzelm
parents: 64167
diff changeset
    84
        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check), options).check
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    85
    }
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    86
  }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    87
}