# HG changeset patch
# User wenzelm
# Date 1693322232 -7200
# Node ID 0e01c3b55b63769e0344859e9b5fe38ef71aa472
# Parent  3f3add5eef919bbc90833101719a970e48396218
clarified signature: prefer enum types;

diff -r 3f3add5eef91 -r 0e01c3b55b63 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Aug 29 17:14:19 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Aug 29 17:17:12 2023 +0200
@@ -395,9 +395,7 @@
 
   val SESSION_NAME = "session_name"
 
-  object Session_Status extends Enumeration {
-    val existing, finished, failed, cancelled = Value
-  }
+  enum Session_Status { case existing, finished, failed, cancelled }
 
   sealed case class Session_Entry(
     chapter: String = "",
@@ -407,7 +405,7 @@
     ml_timing: Timing = Timing.zero,
     sources: Option[String] = None,
     heap_size: Option[Space] = None,
-    status: Option[Session_Status.Value] = None,
+    status: Option[Session_Status] = None,
     errors: List[String] = Nil,
     theory_timings: Map[String, Timing] = Map.empty,
     ml_statistics: List[Properties.T] = Nil
@@ -1129,7 +1127,7 @@
                     Data.ml_timing_gc),
                 sources = res.get_string(Data.sources),
                 heap_size = res.get_long(Data.heap_size).map(Space.bytes),
-                status = res.get_string(Data.status).map(Session_Status.withName),
+                status = res.get_string(Data.status).map(Session_Status.valueOf),
                 errors = uncompress_errors(res.bytes(Data.errors), cache = cache),
                 ml_statistics =
                   if (ml_statistics) {
diff -r 3f3add5eef91 -r 0e01c3b55b63 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Tue Aug 29 17:14:19 2023 +0200
+++ b/src/Pure/Admin/build_status.scala	Tue Aug 29 17:17:12 2023 +0200
@@ -196,7 +196,7 @@
     maximum_heap: Space,
     average_heap: Space,
     stored_heap: Space,
-    status: Build_Log.Session_Status.Value,
+    status: Build_Log.Session_Status,
     errors: List[String]
   ) {
     val date: Long = (afp_pull_date getOrElse pull_date).unix_epoch
@@ -323,7 +323,7 @@
                   maximum_heap = Space.B(ml_stats.maximum(ML_Statistics.HEAP_SIZE)),
                   average_heap = Space.B(ml_stats.average(ML_Statistics.HEAP_SIZE)),
                   stored_heap = Space.bytes(res.long(Build_Log.Data.heap_size)),
-                  status = Build_Log.Session_Status.withName(res.string(Build_Log.Data.status)),
+                  status = Build_Log.Session_Status.valueOf(res.string(Build_Log.Data.status)),
                   errors =
                     Build_Log.uncompress_errors(
                       res.bytes(Build_Log.Data.errors), cache = store.cache))