# HG changeset patch
# User wenzelm
# Date 1688304312 -7200
# Node ID 1ddbeb791f30e56725115b7eddcd113f36575842
# Parent  8c0d3c879f7cc48515c22f88d2e2f9dbca3739d7
more SQL data;

diff -r 8c0d3c879f7c -r 1ddbeb791f30 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sat Jul 01 16:47:52 2023 +0200
+++ b/src/Pure/System/progress.scala	Sun Jul 02 15:25:12 2023 +0200
@@ -57,6 +57,7 @@
     object Agents {
       val agent_uuid = SQL.Column.string("agent_uuid").make_primary_key
       val context_uuid = SQL.Column.string("context_uuid").make_primary_key
+      val kind = SQL.Column.string("kind")
       val hostname = SQL.Column.string("hostname")
       val java_pid = SQL.Column.long("java_pid")
       val java_start = SQL.Column.date("java_start")
@@ -66,7 +67,7 @@
       val seen = SQL.Column.long("seen")
 
       val table = make_table("agents",
-        List(agent_uuid, context_uuid, hostname, java_pid, java_start, start, stamp, stop, seen))
+        List(agent_uuid, context_uuid, kind, hostname, java_pid, java_start, start, stamp, stop, seen))
     }
 
     object Messages {
@@ -238,6 +239,7 @@
 class Database_Progress(
   val db: SQL.Database,
   val base_progress: Progress,
+  val kind: String = "progress",
   val hostname: String = Isabelle_System.hostname(),
   val context_uuid: String = UUID.random().toString)
 extends Progress {
@@ -272,13 +274,14 @@
 
         stmt.string(1) = _agent_uuid
         stmt.string(2) = context_uuid
-        stmt.string(3) = hostname
-        stmt.long(4) = java_pid
-        stmt.date(5) = java_start
-        stmt.date(6) = now
+        stmt.string(3) = kind
+        stmt.string(4) = hostname
+        stmt.long(5) = java_pid
+        stmt.date(6) = java_start
         stmt.date(7) = now
-        stmt.date(8) = None
-        stmt.long(9) = 0L
+        stmt.date(8) = now
+        stmt.date(9) = None
+        stmt.long(10) = 0L
       })
     }
     if (context_uuid == _agent_uuid) Progress.Data.vacuum(db)
diff -r 8c0d3c879f7c -r 1ddbeb791f30 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sat Jul 01 16:47:52 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 15:25:12 2023 +0200
@@ -866,7 +866,8 @@
           val progress =
             new Database_Progress(progress_db, build_progress,
               hostname = hostname,
-              context_uuid = build_uuid)
+              context_uuid = build_uuid,
+              kind = "build_process")
           (progress, progress.agent_uuid)
         }
         catch { case exn: Throwable => close(); throw exn }