# HG changeset patch
# User wenzelm
# Date 1570979860 -7200
# Node ID 8a43ce639d85eefa21b8ae19871d32b6d38e4404
# Parent  85c2cbd35632d5b8d7836af93862caedfd46926d
tuned signature;

diff -r 85c2cbd35632 -r 8a43ce639d85 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Sun Oct 13 16:36:41 2019 +0200
+++ b/src/Pure/Admin/afp.scala	Sun Oct 13 17:17:40 2019 +0200
@@ -20,7 +20,9 @@
       "slow" -> "CPU time much higher than 60min (on mid-range hardware)",
       "very_slow" -> "elapsed time of many hours (on high-end hardware)")
 
-  def groups_bulky: List[String] = List("large", "slow")
+  val groups_bulky: List[String] = List("large", "slow")
+
+  val chapter: String = "AFP"
 
   val force_partition1: List[String] = List("Category3", "HOL-ODE")
 
diff -r 85c2cbd35632 -r 8a43ce639d85 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun Oct 13 16:36:41 2019 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun Oct 13 17:17:40 2019 +0200
@@ -191,11 +191,11 @@
   }
 
   def print_version(
-    isabelle_version: String, afp_version: String = "", chapter: String = "AFP"): String =
+    isabelle_version: String, afp_version: String = "", chapter: String = AFP.chapter): String =
   {
     val body =
       proper_string(isabelle_version).map("Isabelle/" + _).toList :::
-      (if (chapter == "AFP") proper_string(afp_version).map("AFP/" + _) else None).toList
+      (if (chapter == AFP.chapter) proper_string(afp_version).map("AFP/" + _) else None).toList
     if (body.isEmpty) "" else body.mkString(" (", ", ", ")")
   }
 
@@ -335,7 +335,7 @@
                   Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
               }
 
-            if ((!afp || chapter == "AFP") &&
+            if ((!afp || chapter == AFP.chapter) &&
                 (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))
             }