# HG changeset patch
# User wenzelm
# Date 1493456799 -7200
# Node ID 826311fca26351452ffa6c957993a00ffceed02a
# Parent  218dbe4fb484a5326fbf0364498b8d744061f134
tuned;

diff -r 218dbe4fb484 -r 826311fca263 src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Sat Apr 29 10:56:37 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Sat Apr 29 11:06:39 2017 +0200
@@ -427,10 +427,7 @@
 
   object Session_Status extends Enumeration
   {
-    val EXISTING = Value("existing")
-    val FINISHED = Value("finished")
-    val FAILED = Value("failed")
-    val CANCELLED = Value("cancelled")
+    val existing, finished, failed, cancelled = Value
   }
 
   sealed case class Session_Entry(
@@ -445,7 +442,7 @@
   {
     def proper_chapter: Option[String] = if (chapter == "") None else Some(chapter)
     def proper_groups: Option[String] = if (groups.isEmpty) None else Some(cat_lines(groups))
-    def finished: Boolean = status == Session_Status.FINISHED
+    def finished: Boolean = status == Session_Status.finished
   }
 
   object Build_Info
@@ -582,12 +579,12 @@
       Map(
         (for (name <- all_sessions.toList) yield {
           val status =
-            if (failed(name)) Session_Status.FAILED
-            else if (cancelled(name)) Session_Status.CANCELLED
+            if (failed(name)) Session_Status.failed
+            else if (cancelled(name)) Session_Status.cancelled
             else if (timing.isDefinedAt(name) || ml_timing.isDefinedAt(name))
-              Session_Status.FINISHED
-            else if (started(name)) Session_Status.FAILED
-            else Session_Status.EXISTING
+              Session_Status.finished
+            else if (started(name)) Session_Status.failed
+            else Session_Status.existing
           val entry =
             Session_Entry(
               chapter.getOrElse(name, ""),