--- 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"
}