src/Pure/General/mercurial.scala
author wenzelm
Sun, 02 Oct 2016 19:47:18 +0200
changeset 63997 e11ccb5aa82f
child 63998 2f38d8aff2f5
permissions -rw-r--r--
more formal Mercurial support (with the potential to upgrade to command server);
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
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    17
  def opt_rev(rev: String): String = if (rev == "") "" else " --rev " + File.bash_string(rev)
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    18
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    19
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    20
  /* repository access */
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    21
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    22
  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
    23
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    24
  class Repository private[Mercurial](val root: Path)
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
    override def toString: String = root.toString
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    27
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    28
    def close() { }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    29
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    30
    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
    31
      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
    32
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    33
    def manifest(rev: String = "", cwd: JFile = null): List[String] =
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    34
      command("manifest" + opt_rev(rev), cwd = cwd).check.out_lines
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    35
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    36
    command("root").check
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    37
  }
e11ccb5aa82f more formal Mercurial support (with the potential to upgrade to command server);
wenzelm
parents:
diff changeset
    38
}