# HG changeset patch
# User wenzelm
# Date 1678116012 -3600
# Node ID 4af88aca2a4ff813f70169c7d57d35ba4fdd9bf0
# Parent  42c1e5d4ed1479624417d14ef4056b04ceccad13
clarified database content;
tuned signature;

diff -r 42c1e5d4ed14 -r 4af88aca2a4f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Mar 06 16:06:24 2023 +0100
+++ b/src/Pure/Tools/build.scala	Mon Mar 06 16:20:12 2023 +0100
@@ -323,10 +323,10 @@
             soft_build = soft_build,
             export_files = export_files)
         }
-      val end_date = Date.now()
-      val elapsed_time = end_date.time - start_date.time
+      val stop_date = Date.now()
+      val elapsed_time = stop_date.time - start_date.time
 
-      progress.echo("\nFinished at " + Build_Log.print_date(end_date), verbose = true)
+      progress.echo("\nFinished at " + Build_Log.print_date(stop_date), verbose = true)
 
       val total_timing =
         results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
diff -r 42c1e5d4ed14 -r 4af88aca2a4f src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 06 16:06:24 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 06 16:20:12 2023 +0100
@@ -276,9 +276,9 @@
       val ml_platform = SQL.Column.string("ml_platform")
       val options = SQL.Column.string("options")
       val start = SQL.Column.date("start")
-      val end = SQL.Column.date("end")
+      val stop = SQL.Column.date("stop")
 
-      val table = make_table("", List(build_uuid, ml_platform, options, start, end))
+      val table = make_table("", List(build_uuid, ml_platform, options, start, stop))
     }
 
     def start_build(
@@ -297,15 +297,15 @@
         })
     }
 
-    def end_build(db: SQL.Database, build_uuid: String): Unit =
+    def stop_build(db: SQL.Database, build_uuid: String): Unit =
       db.execute_statement(
-        Base.table.update(List(Base.end), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
+        Base.table.update(List(Base.stop), sql = SQL.where(Generic.sql(build_uuid = build_uuid))),
         body = { stmt => stmt.date(1) = db.now() })
 
     def clean_build(db: SQL.Database): Unit = {
       val old =
         db.using_statement(
-          Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.end.defined))
+          Base.table.select(List(Base.build_uuid), sql = SQL.where(Base.stop.defined))
         )(stmt => stmt.execute_query().iterator(_.string(Base.build_uuid)).toList)
 
       if (old.nonEmpty) {
@@ -827,7 +827,7 @@
 
     def exit(): Unit = synchronized_database {
       for (db <- _database) {
-        Build_Process.Data.end_build(db, build_uuid)
+        Build_Process.Data.stop_build(db, build_uuid)
       }
     }