--- a/src/Pure/Admin/build_history.scala Thu Apr 29 15:49:04 2021 +0200
+++ b/src/Pure/Admin/build_history.scala Thu Apr 29 22:39:33 2021 +0200
@@ -532,8 +532,8 @@
ssh: SSH.Session,
isabelle_repos_self: Path,
isabelle_repos_other: Path,
- isabelle_repository: Mercurial.Address = Isabelle_System.isabelle_repository,
- afp_repository: Mercurial.Address = Isabelle_System.afp_repository,
+ isabelle_repository: Mercurial.Server = Isabelle_System.isabelle_repository,
+ afp_repository: Mercurial.Server = Isabelle_System.afp_repository,
isabelle_identifier: String = "remote_build_history",
self_update: Boolean = false,
progress: Progress = new Progress,
@@ -545,7 +545,7 @@
/* Isabelle self repository */
val self_hg =
- Mercurial.setup_repository(isabelle_repository, isabelle_repos_self, ssh = ssh)
+ Mercurial.setup_repository(isabelle_repository.root, isabelle_repos_self, ssh = ssh)
def execute(cmd: String, args: String, echo: Boolean = false, strict: Boolean = true): Unit =
ssh.execute(
@@ -581,7 +581,7 @@
if (afp_rev.isEmpty) ""
else {
val afp_repos = isabelle_repos_other + Path.explode("AFP")
- Mercurial.setup_repository(afp_repository, afp_repos, ssh = ssh)
+ Mercurial.setup_repository(afp_repository.root, afp_repos, ssh = ssh)
" -A " + Bash.string(afp_rev.get)
}
--- a/src/Pure/Admin/isabelle_cronjob.scala Thu Apr 29 15:49:04 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala Thu Apr 29 22:39:33 2021 +0200
@@ -47,8 +47,8 @@
{
Isabelle_Devel.make_index()
- Mercurial.setup_repository(Isabelle_System.isabelle_repository, isabelle_repos)
- Mercurial.setup_repository(Isabelle_System.afp_repository, afp_repos)
+ Mercurial.setup_repository(Isabelle_System.isabelle_repository.root, isabelle_repos)
+ Mercurial.setup_repository(Isabelle_System.afp_repository.root, afp_repos)
File.write(logger.log_dir + Build_Log.log_filename("isabelle_identify", logger.start_date),
Build_Log.Identify.content(logger.start_date, Some(get_rev()), Some(get_afp_rev())))
--- a/src/Pure/General/mercurial.scala Thu Apr 29 15:49:04 2021 +0200
+++ b/src/Pure/General/mercurial.scala Thu Apr 29 22:39:33 2021 +0200
@@ -17,17 +17,41 @@
type Graph = isabelle.Graph[String, Unit]
- /* HTTP server addresses */
+ /* HTTP server */
+
+ object Server
+ {
+ def apply(root: String): Server = new Server(root)
+
+ def start(root: Path): Server =
+ {
+ val hg = repository(root)
- object Address
- {
- def apply(root: String): Address = new Address(root)
+ val server_process = Future.promise[Bash.Process]
+ val server_root = Future.promise[String]
+ Isabelle_Thread.fork("hg") {
+ val process =
+ Exn.capture { Bash.process(hg.command_line("serve", options = "--port 0 --print-url")) }
+ server_process.fulfill_result(process)
+ Exn.release(process).result(progress_stdout =
+ line => if (!server_root.is_finished) {
+ server_root.fulfill(Library.try_unsuffix("/", line).getOrElse(line))
+ })
+ }
+ server_process.join
+
+ new Server(server_root.join) {
+ override def close(): Unit = server_process.join.terminate()
+ }
+ }
}
- final class Address private(val root: String)
+ class Server private(val root: String) extends AutoCloseable
{
override def toString: String = root
+ def close(): Unit = ()
+
def changeset(rev: String = "tip", raw: Boolean = false): String =
root + (if (raw) "/raw-rev/" else "/rev/") + rev
@@ -135,9 +159,8 @@
make_repository(root, "clone",
options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
- def setup_repository(address: Address, root: Path, ssh: SSH.System = SSH.Local): Repository =
+ def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
{
- val source = address.root
if (ssh.is_dir(root)) { val hg = repository(root, ssh = ssh); hg.pull(remote = source); hg }
else clone_repository(source, root, options = "--noupdate", ssh = ssh)
}
@@ -151,14 +174,19 @@
override def toString: String = ssh.hg_url + root.implode
- def command(name: String, args: String = "", options: String = "",
- repository: Boolean = true): Process_Result =
+ def command_line(name: String, args: String = "", options: String = "",
+ repository: Boolean = true): String =
{
- val cmdline =
- "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
- (if (repository) " --repository " + ssh.bash_path(root) else "") +
- " --noninteractive " + name + " " + options + " " + args
- ssh.execute(cmdline)
+ "export LANG=C HGPLAIN=\n\"${HG:-hg}\" --config " + Bash.string("defaults." + name + "=") +
+ (if (repository) " --repository " + ssh.bash_path(root) else "") +
+ " --noninteractive " + name + " " + options + " " + args
+ }
+
+ def command(
+ name: String, args: String = "", options: String = "",
+ repository: Boolean = true): Process_Result =
+ {
+ ssh.execute(command_line(name, args = args, options = options, repository = repository))
}
def add(files: List[Path]): Unit =
--- a/src/Pure/System/isabelle_system.scala Thu Apr 29 15:49:04 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Thu Apr 29 22:39:33 2021 +0200
@@ -621,11 +621,11 @@
/* repositories */
- val isabelle_repository: Mercurial.Address =
- Mercurial.Address("https://isabelle.sketis.net/repos/isabelle")
+ val isabelle_repository: Mercurial.Server =
+ Mercurial.Server("https://isabelle.sketis.net/repos/isabelle")
- val afp_repository: Mercurial.Address =
- Mercurial.Address("https://isabelle.sketis.net/repos/afp-devel")
+ val afp_repository: Mercurial.Server =
+ Mercurial.Server("https://isabelle.sketis.net/repos/afp-devel")
def official_releases(): List[String] =
Library.trim_split_lines(