# HG changeset patch # User wenzelm # Date 1619728773 -7200 # Node ID cc36841eeff6b25b72ade1e08879c630cc377738 # Parent 6ba5f9d18c56de0831b542962dd93deaee9368cf clarified signature: more operations; diff -r 6ba5f9d18c56 -r cc36841eeff6 src/Pure/Admin/build_history.scala --- 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) } diff -r 6ba5f9d18c56 -r cc36841eeff6 src/Pure/Admin/isabelle_cronjob.scala --- 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()))) diff -r 6ba5f9d18c56 -r cc36841eeff6 src/Pure/General/mercurial.scala --- 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 = diff -r 6ba5f9d18c56 -r cc36841eeff6 src/Pure/System/isabelle_system.scala --- 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(