src/Pure/General/mercurial.scala
author wenzelm
Mon, 03 Oct 2016 21:36:10 +0200
changeset 64027 4a33d740c9dc
parent 64020 355b78441650
child 64028 6cc79f1c82cd
permissions -rw-r--r--
proper log output;
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
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    27
  def open_repository(root: Path): Repository = new Repository(root)
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    28
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    29
  class Repository private[Mercurial](val root: Path)
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
    override def toString: String = root.toString
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    32
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    33
    def close() { }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    34
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    35
    def command(cmd: String, cwd: JFile = null): Process_Result =
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    36
      Isabelle_System.hg("--repository " + File.bash_path(root) + " " + cmd, cwd = cwd)
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    37
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    38
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    39
    def heads(template: String = "{node|short}\n", options: String = ""): List[String] =
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    40
      command("heads " + options + opt_template(template)).check.out_lines
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    41
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    42
    def identify(rev: String = "", options: String = ""): String =
64020
355b78441650 clarified: a variant of -i is the default, but its output is not as precise as it might seem;
wenzelm
parents: 63999
diff changeset
    43
      command("id " + options + opt_rev(rev)).check.out_lines.headOption getOrElse ""
63998
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    44
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    45
    def manifest(rev: String = "", options: String = ""): List[String] =
2f38d8aff2f5 more operations;
wenzelm
parents: 63997
diff changeset
    46
      command("manifest " + options + opt_rev(rev)).check.out_lines
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    47
64027
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
    48
    def log(rev: String = "", options: String = ""): String =
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
    49
      Library.trim_line(command("log " + options + opt_rev(rev)).check.out)
4a33d740c9dc proper log output;
wenzelm
parents: 64020
diff changeset
    50
63999
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    51
    def pull(remote: String = "", rev: String = "", options: String = ""): Unit =
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    52
      command("pull " + options + opt_rev(rev) + optional(remote)).check
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    53
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    54
    def update(rev: String = "", clean: Boolean = false, check: Boolean = false, options: String = "")
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    55
    {
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    56
      command("update " + options +
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    57
        opt_rev(rev) + opt_flag("--clean", clean) + opt_flag("--check", check)).check
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    58
    }
5649a993666d more operations;
wenzelm
parents: 63998
diff changeset
    59
63997
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    60
    command("root").check
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    61
  }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    62
}