clarified signature: more operations;
authorwenzelm
Thu, 29 Apr 2021 22:39:33 +0200
changeset 73867 cc36841eeff6
parent 73866 6ba5f9d18c56
child 73868 f28df88c0d00
clarified signature: more operations;
src/Pure/Admin/build_history.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/General/mercurial.scala
src/Pure/System/isabelle_system.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)
       }
 
--- 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(