# HG changeset patch
# User wenzelm
# Date 1619644805 -7200
# Node ID 58b17dca57ef40e9defb292c7820a4743029cac5
# Parent  6081885b9d06a49cbd2b425d20ad40e163a22e09
clarified signature;

diff -r 6081885b9d06 -r 58b17dca57ef src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Wed Apr 28 14:03:26 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Wed Apr 28 23:20:05 2021 +0200
@@ -532,8 +532,8 @@
     ssh: SSH.Session,
     isabelle_repos_self: Path,
     isabelle_repos_other: Path,
-    isabelle_repos_source: String = Isabelle_System.isabelle_repository,
-    afp_repos_source: String = Isabelle_System.afp_repository,
+    isabelle_repository: Mercurial.Address = Isabelle_System.isabelle_repository,
+    afp_repository: Mercurial.Address = 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_repos_source, isabelle_repos_self, ssh = ssh)
+      Mercurial.setup_repository(isabelle_repository, 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_repos_source, afp_repos, ssh = ssh)
+        Mercurial.setup_repository(afp_repository, afp_repos, ssh = ssh)
         " -A " + Bash.string(afp_rev.get)
       }
 
diff -r 6081885b9d06 -r 58b17dca57ef src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Wed Apr 28 14:03:26 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 28 23:20:05 2021 +0200
@@ -759,10 +759,10 @@
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
-        HTML.link(Isabelle_System.isabelle_repository + "/rev/" + release.ident,
+        HTML.link(Isabelle_System.isabelle_repository.rev(release.ident),
           HTML.text("Isabelle/" + release.ident))
       val afp_link =
-        HTML.link(Isabelle_System.afp_repository + "/rev/" + afp_rev, HTML.text("AFP/" + afp_rev))
+        HTML.link(Isabelle_System.afp_repository.rev(afp_rev), HTML.text("AFP/" + afp_rev))
 
       HTML.write_document(dir, "index.html",
         List(HTML.title(release.dist_name)),
diff -r 6081885b9d06 -r 58b17dca57ef src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Wed Apr 28 14:03:26 2021 +0200
+++ b/src/Pure/General/mercurial.scala	Wed Apr 28 23:20:05 2021 +0200
@@ -8,8 +8,6 @@
 package isabelle
 
 
-import java.io.{File => JFile}
-
 import scala.annotation.tailrec
 import scala.collection.mutable
 
@@ -19,6 +17,21 @@
   type Graph = isabelle.Graph[String, Unit]
 
 
+  /* HTTP server addresses */
+
+  object Address
+  {
+    def apply(root: String): Address = new Address(root)
+  }
+
+  final class Address private(val root: String)
+  {
+    override def toString: String = root
+
+    def rev(r: String): String = root + "/rev/" + r
+  }
+
+
   /* command-line syntax */
 
   def optional(s: String, prefix: String = ""): String =
@@ -93,8 +106,9 @@
     make_repository(root, "clone",
       options + " " + Bash.string(source) + " " + ssh.bash_path(root) + opt_rev(rev), ssh = ssh)
 
-  def setup_repository(source: String, root: Path, ssh: SSH.System = SSH.Local): Repository =
+  def setup_repository(address: Address, 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)
   }
diff -r 6081885b9d06 -r 58b17dca57ef src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Wed Apr 28 14:03:26 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 28 23:20:05 2021 +0200
@@ -621,7 +621,9 @@
 
   /* repositories */
 
-  val isabelle_repository: String = "https://isabelle.sketis.net/repos/isabelle"
+  val isabelle_repository: Mercurial.Address =
+    Mercurial.Address("https://isabelle.sketis.net/repos/isabelle")
 
-  val afp_repository: String = "https://isabelle.sketis.net/repos/afp-devel"
+  val afp_repository: Mercurial.Address =
+    Mercurial.Address("https://isabelle.sketis.net/repos/afp-devel")
 }