tuned signature;
authorwenzelm
Wed, 28 Apr 2021 14:03:26 +0200
changeset 73864 6081885b9d06
parent 73863 fc13738e1933
child 73865 58b17dca57ef
tuned signature;
src/Pure/Admin/afp.scala
src/Pure/Admin/build_history.scala
src/Pure/Admin/build_release.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/System/isabelle_system.scala
--- a/src/Pure/Admin/afp.scala	Wed Apr 28 13:03:09 2021 +0200
+++ b/src/Pure/Admin/afp.scala	Wed Apr 28 14:03:26 2021 +0200
@@ -13,8 +13,6 @@
 
 object AFP
 {
-  val repos_source = "https://isabelle.sketis.net/repos/afp-devel"
-
   val groups: Map[String, String] =
     Map("large" -> "full 64-bit memory model or word arithmetic required",
       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
--- a/src/Pure/Admin/build_history.scala	Wed Apr 28 13:03:09 2021 +0200
+++ b/src/Pure/Admin/build_history.scala	Wed Apr 28 14:03:26 2021 +0200
@@ -532,8 +532,8 @@
     ssh: SSH.Session,
     isabelle_repos_self: Path,
     isabelle_repos_other: Path,
-    isabelle_repos_source: String = Isabelle_Cronjob.isabelle_repos_source,
-    afp_repos_source: String = AFP.repos_source,
+    isabelle_repos_source: String = Isabelle_System.isabelle_repository,
+    afp_repos_source: String = Isabelle_System.afp_repository,
     isabelle_identifier: String = "remote_build_history",
     self_update: Boolean = false,
     progress: Progress = new Progress,
--- a/src/Pure/Admin/build_release.scala	Wed Apr 28 13:03:09 2021 +0200
+++ b/src/Pure/Admin/build_release.scala	Wed Apr 28 14:03:26 2021 +0200
@@ -759,10 +759,10 @@
         } yield (bundle_info.name, bundle_info)
 
       val isabelle_link =
-        HTML.link(Isabelle_Cronjob.isabelle_repos_source + "/rev/" + release.ident,
+        HTML.link(Isabelle_System.isabelle_repository + "/rev/" + release.ident,
           HTML.text("Isabelle/" + release.ident))
       val afp_link =
-        HTML.link(AFP.repos_source + "/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)),
--- a/src/Pure/Admin/isabelle_cronjob.scala	Wed Apr 28 13:03:09 2021 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Wed Apr 28 14:03:26 2021 +0200
@@ -22,7 +22,6 @@
   val current_log: Path = main_dir + Path.explode("run/main.log")  // owned by log service
   val cumulative_log: Path = main_dir + Path.explode("log/main.log")  // owned by log service
 
-  val isabelle_repos_source = "https://isabelle.sketis.net/repos/isabelle"
   val isabelle_repos: Path = main_dir + Path.explode("isabelle")
   val afp_repos: Path = main_dir + Path.explode("AFP")
 
@@ -48,8 +47,8 @@
       {
         Isabelle_Devel.make_index()
 
-        Mercurial.setup_repository(isabelle_repos_source, isabelle_repos)
-        Mercurial.setup_repository(AFP.repos_source, afp_repos)
+        Mercurial.setup_repository(Isabelle_System.isabelle_repository, isabelle_repos)
+        Mercurial.setup_repository(Isabelle_System.afp_repository, 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/System/isabelle_system.scala	Wed Apr 28 13:03:09 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala	Wed Apr 28 14:03:26 2021 +0200
@@ -617,4 +617,11 @@
     override def invoke(args: List[Bytes]): List[Bytes] =
       args match { case List(url) => List(download(url.text).bytes) }
   }
+
+
+  /* repositories */
+
+  val isabelle_repository: String = "https://isabelle.sketis.net/repos/isabelle"
+
+  val afp_repository: String = "https://isabelle.sketis.net/repos/afp-devel"
 }