# HG changeset patch
# User wenzelm
# Date 1711639656 -3600
# Node ID 42bc8ab751c177d0e30881da3d94994e7295e285
# Parent  f8d7df38d7c668946e1e12984f0948f5501f2b39
clarified modules: more official Sessions.notable_groups;

diff -r f8d7df38d7c6 -r 42bc8ab751c1 src/Pure/Admin/afp.scala
--- a/src/Pure/Admin/afp.scala	Thu Mar 28 16:14:28 2024 +0100
+++ b/src/Pure/Admin/afp.scala	Thu Mar 28 16:27:36 2024 +0100
@@ -12,13 +12,6 @@
 
 
 object AFP {
-  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)",
-      "very_slow" -> "elapsed time of many hours (on high-end hardware)")
-
-  val groups_bulky: List[String] = List("large", "slow")
-
   val chapter: String = "AFP"
 
   val BASE: Path = Path.explode("$AFP_BASE")
diff -r f8d7df38d7c6 -r 42bc8ab751c1 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Thu Mar 28 16:14:28 2024 +0100
+++ b/src/Pure/Admin/build_status.scala	Thu Mar 28 16:27:36 2024 +0100
@@ -354,7 +354,7 @@
 
               if (session.isDefined &&
                   (!afp || chapter == AFP.chapter) &&
-                  (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
+                  (!profile.bulky || groups.exists(Sessions.bulky_groups))) {
                 data_entries += (data_name -> (sessions + (session_name -> session.get)))
               }
             }
diff -r f8d7df38d7c6 -r 42bc8ab751c1 src/Pure/Build/sessions.scala
--- a/src/Pure/Build/sessions.scala	Thu Mar 28 16:14:28 2024 +0100
+++ b/src/Pure/Build/sessions.scala	Thu Mar 28 16:27:36 2024 +0100
@@ -530,6 +530,37 @@
   }
 
 
+  /* notable groups */
+
+  sealed case class Group_Info(
+    name: String,
+    description: String,
+    bulky: Boolean = false,
+    afp: Boolean = false
+  ) {
+    override def toString: String = name
+  }
+
+  lazy val notable_groups: List[Group_Info] =
+    List(
+      Group_Info("large", "full 64-bit memory model or word arithmetic required",
+        bulky = true, afp = true),
+      Group_Info("slow", "CPU time much higher than 60min (on mid-range hardware)",
+        bulky = true, afp = true),
+      Group_Info("very_slow", "elapsed time of many hours (on high-end hardware)",
+        afp = true),
+      Group_Info("AFP", "entry within AFP", afp = true),
+      Group_Info("doc", "Isabelle documentation"),
+      Group_Info("no_doc", "suppressed Isabelle documentation")
+    )
+
+  lazy val bulky_groups: Set[String] =
+    Set.from(notable_groups.flatMap(g => if (g.bulky) Some(g.name) else None))
+
+  lazy val afp_groups: Set[String] =
+    Set.from(notable_groups.flatMap(g => if (g.afp) Some(g.name) else None))
+
+
   /* cumulative session info */
 
   private val BUILD_PREFS_BG = "<build_prefs:"
@@ -740,7 +771,7 @@
     def record_proofs: Boolean = options.int("record_proofs") >= 2
 
     def is_afp: Boolean = chapter == AFP.chapter
-    def is_afp_bulky: Boolean = is_afp && groups.exists(AFP.groups_bulky.contains)
+    def is_afp_bulky: Boolean = is_afp && groups.exists(bulky_groups)
   }
 
   object Selection {