src/Pure/Tools/build_schedule.scala

     type Graph = isabelle.Graph[String, Node]
 
     def init(build_uuid: String): Schedule = Schedule(build_uuid, "none", Date.now(), Graph.empty)
   }
 
-  case class Schedule(build_uuid: String, generator: String, start: Date, graph: Schedule.Graph) {
+  case class Schedule(
+    build_uuid: String,
+    generator: String,
+    start: Date,
+    graph: Schedule.Graph,
+    serial: Long = 0,
+  ) {
+    require(serial >= 0, "serial underflow")
+    def inc_serial: Schedule = {
+      require(serial < Long.MaxValue, "serial overflow")
+      copy(serial = serial + 1)
+    }
+    
     def end: Date =
       if (graph.is_empty) start
       else graph.maximals.map(graph.get_node).map(_.end).maxBy(_.unix_epoch)
 
     def duration: Time = end.time - start.time

           case Some(db) =>
             Build_Schedule.private_data.transaction_lock(db, label = label) {
               val old_schedule = Build_Schedule.private_data.pull_schedule(db, _schedule)
               _schedule = old_schedule
               val res = body
-              Build_Schedule.private_data.update_schedule(db, _schedule)
+              _schedule = Build_Schedule.private_data.update_schedule(db, _schedule, old_schedule)
               res
             }
         }
       }
 

 
     object Schedules {
       val build_uuid = Generic.build_uuid.make_primary_key
       val generator = SQL.Column.string("generator")
       val start = SQL.Column.date("start")
-
-      val table = make_table(List(build_uuid, generator, start), name = "schedules")
-    }
+      val serial = SQL.Column.long("serial")
+
+      val table = make_table(List(build_uuid, generator, start, serial), name = "schedules")
+    }
+
+    def read_serial(db: SQL.Database, build_uuid: String = ""): Long =
+      db.execute_query_statementO[Long](
+        Schedules.table.select(List(Schedules.serial.max), sql = 
+          SQL.where(if_proper(build_uuid, Schedules.build_uuid.equal(build_uuid)))),
+          _.long(Schedules.serial)).getOrElse(0L)
 
     def read_scheduled_builds_domain(db: SQL.Database): List[String] =
       db.execute_query_statement(
         Schedules.table.select(List(Schedules.build_uuid)),
         List.from[String], res => res.string(Schedules.build_uuid))

         val nodes = private_data.read_nodes(db, build_uuid = schedule.build_uuid)
         schedule.copy(graph = Graph.make(nodes))
       }
     }
 
-    def update_schedule(db: SQL.Database, schedule: Schedule): Unit = {
+    def write_schedule(db: SQL.Database, schedule: Schedule): Unit = {
       db.execute_statement(
         Schedules.table.delete(Schedules.build_uuid.where_equal(schedule.build_uuid)))
       db.execute_statement(Schedules.table.insert(), { stmt =>
         stmt.string(1) = schedule.build_uuid
         stmt.string(2) = schedule.generator
         stmt.date(3) = schedule.start
+        stmt.long(4) = schedule.serial
       })
       update_nodes(db, schedule.build_uuid, schedule.graph.dest)
     }
 
 

           stmt.date(7) = node.start
           stmt.long(8) = node.duration.ms
         })
     }
 
-    def pull_schedule(
-      db: SQL.Database,
-      schedule: Schedule,
-    ): Build_Schedule.Schedule =
-      read_schedules(db, schedule.build_uuid) match {
-        case Nil => schedule
-        case schedules => Library.the_single(schedules)
-      }
+    def pull_schedule(db: SQL.Database, old_schedule: Schedule): Build_Schedule.Schedule = {
+      val serial_db = read_serial(db)
+      if (serial_db == old_schedule.serial) old_schedule
+      else {
+        read_schedules(db, old_schedule.build_uuid) match {
+          case Nil => old_schedule
+          case schedules => Library.the_single(schedules)
+        }
+      }
+    }
+
+    def update_schedule(db: SQL.Database, schedule: Schedule, old_schedule: Schedule): Schedule = {
+      val changed =
+        schedule.generator != old_schedule.generator ||
+        schedule.start != old_schedule.start ||
+        schedule.graph != old_schedule.graph
+      
+      val schedule1 =
+        if (changed) schedule.copy(serial = old_schedule.serial).inc_serial else schedule
+      if (schedule1.serial != schedule.serial) write_schedule(db, schedule1)
+      
+      schedule1
+    }
 
     def remove_schedules(db: SQL.Database, remove: List[String]): Unit =
       if (remove.nonEmpty) {
         val sql = Generic.build_uuid.where_member(remove)
         db.execute_statement(SQL.MULTI(tables.map(_.delete(sql = sql))))