src/Pure/General/mercurial.scala
changeset 73611 cc36841eeff6
parent 73610 6ba5f9d18c56
child 73624 f033d4f661e9
equal deleted inserted replaced
73610:6ba5f9d18c56 73611:cc36841eeff6
    15 object Mercurial
    15 object Mercurial
    16 {
    16 {
    17   type Graph = isabelle.Graph[String, Unit]
    17   type Graph = isabelle.Graph[String, Unit]
    18 
    18 
    19 
    19 
    20   /* HTTP server addresses */
    20   /* HTTP server */
    21 
    21 
    22   object Address
    22   object Server
    23   {
    23   {
    24     def apply(root: String): Address = new Address(root)
    24     def apply(root: String): Server = new Server(root)
    25   }
    25 
    26 
    26     def start(root: Path): Server =
    27   final class Address private(val root: String)
    27     {
       
    28       val hg = repository(root)
       
    29 
       
    30       val server_process = Future.promise[Bash.Process]
       
    31       val server_root = Future.promise[String]
       
    32       Isabelle_Thread.fork("hg") {
       
    33         val process =
       
    34           Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
       
    35         server_process.fulfill_result(process)
       
    36         Exn.release(process).result(progress_stdout =
       
    37           line => if (!server_root.is_finished) {
       
    38             server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line))
       
    39           })
       
    40       }
       
    41       server_process.join
       
    42 
       
    43       new Server(server_root.join) {
       
    44         override def close(): Unit = server_process.join.terminate()
       
    45       }
       
    46     }
       
    47   }
       
    48 
       
    49   class Server private(val root: String) extends AutoCloseable
    28   {
    50   {
    29     override def toString: String = root
    51     override def toString: String = root
       
    52 
       
    53     def close(): Unit = ()
    30 
    54 
    31     def changeset(rev: String = "tip", raw: Boolean = false): String =
    55     def changeset(rev: String = "tip", raw: Boolean = false): String =
    32       root + (if (raw) "/raw-rev/" else "/rev/") + rev
    56       root + (if (raw) "/raw-rev/" else "/rev/") + rev
    33 
    57 
    34     def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
    58     def file(path: Path, rev: String = "tip", raw: Boolean = false): String =
   133   def clone_repository(source: String, root: Path,
   157   def clone_repository(source: String, root: Path,
   134       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
   158       rev: String = "", options: String = "", ssh: SSH.System = SSH.Local): Repository =
   135     make_repository(root, "clone",
   159     make_repository(root, "clone",
   136       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
   160       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
   137 
   161 
   138   def setup_repository(address: Address, root: Path, ssh: SSH.System = SSH.Local): Repository =
   162   def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
   139   {
   163   {
   140     val source = address.root
       
   141     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
   164     if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
   142     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   165     else clone_repository(source, root, options = "--noupdate", ssh = ssh)
   143   }
   166   }
   144 
   167 
   145   class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
   168   class Repository private[Mercurial](root_path: Path, ssh: SSH.System = SSH.Local)
   149     val root: Path = ssh.expand_path(root_path)
   172     val root: Path = ssh.expand_path(root_path)
   150     def root_url: String = ssh.hg_url + root.implode
   173     def root_url: String = ssh.hg_url + root.implode
   151 
   174 
   152     override def toString: String = ssh.hg_url + root.implode
   175     override def toString: String = ssh.hg_url + root.implode
   153 
   176 
   154     def command(name: String, args: String = "", options: String = "",
   177     def command_line(name: String, args: String = "", options: String = "",
   155       repository: Boolean = true): Process_Result =
   178       repository: Boolean = true): String =
   156     {
   179     {
   157       val cmdline =
   180       "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
   158         "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
   181         (if (repository) " --repository " + ssh.bash_path(root) else "") +
   159           (if (repository) " --repository " + ssh.bash_path(root) else "") +
   182         " --noninteractive " + name + " " + options + " " + args
   160           " --noninteractive " + name + " " + options + " " + args
   183     }
   161       ssh.execute(cmdline)
   184 
       
   185     def command(
       
   186       name: String, args: String = "", options: String = "",
       
   187       repository: Boolean = true):  Process_Result =
       
   188     {
       
   189       ssh.execute(command_line(name, args = args, options = options, repository = repository))
   162     }
   190     }
   163 
   191 
   164     def add(files: List[Path]): Unit =
   192     def add(files: List[Path]): Unit =
   165       hg.command("add", files.map(ssh.bash_path).mkString(" "))
   193       hg.command("add", files.map(ssh.bash_path).mkString(" "))
   166 
   194