# HG changeset patch
# User wenzelm
# Date 1709656956 -3600
# Node ID a8d7cf8acaa688496351919f1d6a38f236e3198d
# Parent  8e17f585177fec2ae24323493d84a637ea0d1feb
drop unused Task.info field;

diff -r 8e17f585177f -r a8d7cf8acaa6 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 05 17:27:16 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 05 17:42:36 2024 +0100
@@ -43,7 +43,6 @@
   sealed case class Task(
     name: String,
     deps: List[String],
-    info: JSON.Object.T,
     build_uuid: String
   ) {
     def is_ready: Boolean = deps.isEmpty
@@ -566,10 +565,9 @@
     object Pending {
       val name = Generic.name.make_primary_key
       val deps = SQL.Column.string("deps")
-      val info = SQL.Column.string("info")
       val build_uuid = Generic.build_uuid
 
-      val table = make_table(List(name, deps, info, build_uuid), name = "pending")
+      val table = make_table(List(name, deps, build_uuid), name = "pending")
     }
 
     def read_pending(db: SQL.Database): List[Task] =
@@ -579,9 +577,8 @@
         { res =>
           val name = res.string(Pending.name)
           val deps = res.string(Pending.deps)
-          val info = res.string(Pending.info)
           val build_uuid = res.string(Pending.build_uuid)
-          Task(name, split_lines(deps), JSON.Object.parse(info), build_uuid)
+          Task(name, split_lines(deps), build_uuid)
         })
 
     def update_pending(
@@ -601,8 +598,7 @@
           for (task <- insert) yield { (stmt: SQL.Statement) =>
             stmt.string(1) = task.name
             stmt.string(2) = cat_lines(task.deps)
-            stmt.string(3) = JSON.Format(task.info)
-            stmt.string(4) = task.build_uuid
+            stmt.string(3) = task.build_uuid
           })
       }
 
@@ -978,7 +974,7 @@
     val new_pending =
       List.from(
         for (session <- sessions1.iterator if !old_pending(session.name))
-          yield Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_uuid))
+          yield Build_Process.Task(session.name, session.deps, build_uuid))
     val pending1 = new_pending ::: state.pending
 
     state.copy(sessions = sessions1, pending = pending1)
diff -r 8e17f585177f -r a8d7cf8acaa6 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Tue Mar 05 17:27:16 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Tue Mar 05 17:42:36 2024 +0100
@@ -1328,7 +1328,7 @@
 
       val sessions = Build_Process.Sessions.empty.init(build_context, database_server, progress)
       def task(session: Build_Job.Session_Context): Build_Process.Task =
-        Build_Process.Task(session.name, session.deps, JSON.Object.empty, build_context.build_uuid)
+        Build_Process.Task(session.name, session.deps, build_context.build_uuid)
 
       val build_state =
         Build_Process.State(sessions = sessions, pending = sessions.iterator.map(task).toList)